Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_7963a4bf2feda239add5cf25163811bc2206f6f21a0e4a70277699970e74fa1e with
x0,
x1,
∃ x2 . and (Subq x2 x1) (equip x0 x2) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι → ι be given.
Apply unknownprop_6a8f953ba7c3bf327e583b76a91b24ddd499843a498fbfe2514e26f3800e68b3 with
x0,
x1,
x2,
∃ x3 . and (Subq x3 x1) (equip x0 x3) leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H2:
∀ x3 . In x3 x0 ⟶ In (x2 x3) x1.
Assume H3:
∀ x3 . In x3 x0 ⟶ ∀ x4 . In x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4.
Let x3 of type ο be given.
Apply H4 with
Repl x0 (λ x4 . x2 x4).
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
Subq (Repl x0 (λ x4 . x2 x4)) x1,
equip x0 (Repl x0 (λ x4 . x2 x4)) leaving 2 subgoals.
Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
Repl x0 (λ x4 . x2 x4),
x1.
Let x4 of type ι be given.
Assume H5:
In x4 (Repl x0 (λ x5 . x2 x5)).
Apply unknownprop_89e422bb3b8a01dd209d7f2f210df650a435fc3e6005e0f59c57a5e7a59a6d0e with
x0,
x2,
x4,
In x4 x1 leaving 2 subgoals.
The subproof is completed by applying H5.
Let x5 of type ι be given.
Assume H7: x4 = x2 x5.
Apply H7 with
λ x6 x7 . In x7 x1.
Apply H2 with
x5.
The subproof is completed by applying H6.
Apply unknownprop_4b95783dcb3eee1943e1de5542f675166ef402c8fbdda80bdf0920b55d3fc6de with
x0,
Repl x0 (λ x4 . x2 x4),
x2.
Apply unknownprop_aa42ade5598d8612d2029318c4ed81646c550ecc6cdd9ab953ce4bf73f3dd562 with
x0,
Repl x0 x2,
x2 leaving 2 subgoals.
Apply unknownprop_57c8600e4bc6abecef2ae17962906fa2de1fc16f5d46ed100ff99cd5b67f5b1b with
x0,
Repl x0 x2,
x2 leaving 2 subgoals.
Let x4 of type ι be given.
Apply unknownprop_63c308b92260dbfca8c9530846e6836ba3e6be221cc8e80fd61db913e01bdacf with
x0,
x2,
x4.
The subproof is completed by applying H5.
The subproof is completed by applying H3.
Let x4 of type ι be given.
Assume H5:
In x4 (Repl x0 (λ x5 . x2 x5)).
Apply unknownprop_89e422bb3b8a01dd209d7f2f210df650a435fc3e6005e0f59c57a5e7a59a6d0e with
x0,
x2,
x4,
∃ x5 . and (In x5 x0) (x2 x5 = x4) leaving 2 subgoals.
The subproof is completed by applying H5.
Let x5 of type ι be given.
Assume H7: x4 = x2 x5.
Let x6 of type ο be given.
Assume H8:
∀ x7 . and (In x7 x0) (x2 x7 = x4) ⟶ x6.
Apply H8 with
x5.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
In x5 x0,
x2 x5 = x4 leaving 2 subgoals.
The subproof is completed by applying H6.
Let x7 of type ι → ι → ο be given.
The subproof is completed by applying H7 with λ x8 x9 . x7 x9 x8.