Let x0 of type ι → ο be given.
Let x1 of type ι → ι be given.
Let x2 of type ι be given.
Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with
exactly3 x2.
Claim L2:
∃ x3 . In x3 x2Apply unknownprop_b777a79c17f16cd28153af063df26a4626b11c1f1d4394d7f537c11837ab0962 with
∃ x3 . In x3 x2.
Assume H2:
not (∃ x3 . In x3 x2).
Apply unknownprop_c29e201c2636d12615b11e1220001fcc0c2bbdeb53735eb34683c60a05a28860 with
atleast3 x2,
not (atleast4 x2).
Apply unknownprop_c9103b15101bbc1f738ceaf0919de1c89b5c7611420a12711eed9f8143f9b582 with
x2.
The subproof is completed by applying H1.
Apply unknownprop_8ba3cc049a46be464fc77cd637cbc117a0f7ace4cdc85587acac7999a5948772 with
x2,
False leaving 2 subgoals.
The subproof is completed by applying L3.
Let x3 of type ι be given.
Apply andE with
Subq x3 x2,
and (not (Subq x2 x3)) (atleast2 x3),
False leaving 2 subgoals.
The subproof is completed by applying H4.
Apply notE with
Subq x2 x3 leaving 2 subgoals.
Apply unknownprop_c29e201c2636d12615b11e1220001fcc0c2bbdeb53735eb34683c60a05a28860 with
not (Subq x2 x3),
atleast2 x3.
The subproof is completed by applying H6.
Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
x2,
x3.
Let x4 of type ι be given.
Apply FalseE with
In x4 x3.
Apply notE with
∃ x5 . In x5 x2 leaving 2 subgoals.
The subproof is completed by applying H2.
Let x5 of type ο be given.
Assume H8:
∀ x6 . In x6 x2 ⟶ x5.
Apply H8 with
x4.
The subproof is completed by applying H7.
Apply L2 with
False.
Let x3 of type ι be given.
Assume H3:
(λ x4 . In x4 x2) x3.
Apply H0 with
x3,
0 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying unknownprop_48b433c7921d49bb7e4205d5d86f68a84030c1b7df98f7a59f08a308cb665298 with x2.
Apply notE with
TransSet 0 leaving 2 subgoals.
Apply unknownprop_691e57c539f219e8b63c6900720d2387f320621de398fcaf8bd5551ad6c0dc08 with
0.
The subproof is completed by applying unknownprop_0e150139fedb8d7a0ae85e3054b4c73c936e7acb880ce730fb00a0093c9c6c27.