Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Assume H1:
∀ x2 . In x2 x0 ⟶ In (x1 x2) x0.
Assume H2:
∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3.
Apply unknownprop_aa42ade5598d8612d2029318c4ed81646c550ecc6cdd9ab953ce4bf73f3dd562 with
x0,
x0,
x1 leaving 2 subgoals.
Apply unknownprop_57c8600e4bc6abecef2ae17962906fa2de1fc16f5d46ed100ff99cd5b67f5b1b with
x0,
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Let x2 of type ι be given.
Apply unknownprop_b777a79c17f16cd28153af063df26a4626b11c1f1d4394d7f537c11837ab0962 with
∃ x3 . and (In x3 x0) (x1 x3 = x2).
Assume H4:
not (∃ x3 . and (In x3 x0) (x1 x3 = x2)).
Apply notE with
∀ x3 . In x3 (ordsucc x0) ⟶ ∀ x4 . In x4 (ordsucc x0) ⟶ (λ x5 . If_i (x5 = x0) x2 (x1 x5)) x3 = (λ x5 . If_i (x5 = x0) x2 (x1 x5)) x4 ⟶ x3 = x4 leaving 2 subgoals.
The subproof is completed by applying L5.
Let x3 of type ι be given.
Let x4 of type ι be given.
Apply unknownprop_b257b354d80b58d9a8444b167a21f47b4aabc910dc3698404491d5ef01e18cf3 with
x3 = x0,
If_i (x3 = x0) x2 (x1 x3) = If_i (x4 = x0) x2 (x1 x4) ⟶ x3 = x4 leaving 2 subgoals.
Assume H10: x3 = x0.
Apply unknownprop_b257b354d80b58d9a8444b167a21f47b4aabc910dc3698404491d5ef01e18cf3 with
x4 = x0,
If_i (x3 = x0) x2 (x1 x3) = If_i (x4 = x0) x2 (x1 x4) ⟶ x3 = x4 leaving 2 subgoals.
Assume H11: x4 = x0.
Assume H12:
If_i (x3 = x0) x2 (x1 x3) = If_i (x4 = x0) x2 (x1 x4).
Apply H11 with
λ x5 x6 . x3 = x6.
The subproof is completed by applying H10.
Assume H11:
not (x4 = x0).
Apply unknownprop_6f44febdf8a865ee94133af873e3c2941a931de6ac80968301360290e02ca608 with
x3 = x0,
x2,
x1 x3,
λ x5 x6 . x6 = If_i (x4 = x0) x2 (x1 x4) ⟶ x3 = x4 leaving 2 subgoals.
The subproof is completed by applying H10.
Apply unknownprop_5a150bd86f4285de5d98c60b17d4452a655b4d88de0a02247259cdad6e6d992c with
x4 = x0,
x2,
x1 x4,
λ x5 x6 . x2 = x6 ⟶ x3 = x4 leaving 2 subgoals.
The subproof is completed by applying H11.
Assume H12: x2 = x1 x4.
Apply FalseE with
x3 = x4.
Apply notE with
∃ x5 . and (In x5 x0) (x1 x5 = x2) leaving 2 subgoals.
The subproof is completed by applying H4.
Let x5 of type ο be given.
Assume H13:
∀ x6 . and (In x6 x0) (x1 x6 = x2) ⟶ x5.
Apply H13 with
x4.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
In x4 x0,
x1 x4 = x2 leaving 2 subgoals.
Apply L9.
The subproof is completed by applying H11.
Let x6 of type ι → ι → ο be given.
The subproof is completed by applying H12 with λ x7 x8 . x6 x8 x7.
Assume H10:
not (x3 = x0).
Apply unknownprop_b257b354d80b58d9a8444b167a21f47b4aabc910dc3698404491d5ef01e18cf3 with
x4 = x0,
If_i (x3 = x0) x2 (x1 x3) = If_i (x4 = x0) x2 (x1 ...) ⟶ x3 = x4 leaving 2 subgoals.