Apply unknownprop_acac0f89c78f08b97a9fe27ba4af5f929f74e43a9a77a0beb38d70975279c8b8 with
λ x0 . ∀ x1 . or (In x0 (V_ x1)) (Subq (V_ x1) (V_ x0)).
Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_80056f9db85f84f8ce0644e1cdb62f5e66ec62c041f28dd7a07b3c46de1ea696 with
x0,
V_ x1,
or (In x0 (V_ x1)) (Subq (V_ x1) (V_ x0)) leaving 2 subgoals.
Assume H1:
In x0 (V_ x1).
Apply unknownprop_7c688f24c3595bc4b513e911d7f551c8ccfedc804a6c15c02d25d01a2996aec6 with
In x0 (V_ x1),
Subq (V_ x1) (V_ x0).
The subproof is completed by applying H1.
Assume H1:
nIn x0 (V_ x1).
Apply unknownprop_c29620ea10188dd8ed7659bc2875dc8e08f16ffd29713f8ee3146f02f9828ceb with
In x0 (V_ x1),
Subq (V_ x1) (V_ x0).
Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
V_ x1,
V_ x0.
Let x2 of type ι be given.
Assume H2:
In x2 (V_ x1).
Apply unknownprop_3687558d9284fdd514174bfe87bba39032212334a6409eb4554d4077dea6d831 with
x2,
x1,
In x2 (V_ x0) leaving 2 subgoals.
The subproof is completed by applying H2.
Let x3 of type ι be given.
Apply unknownprop_b777a79c17f16cd28153af063df26a4626b11c1f1d4394d7f537c11837ab0962 with
∃ x4 . and (In x4 x0) (nIn x4 (V_ x3)).
Apply unknownprop_8369708f37c0d20e10b6156293f1b207e835dfc563ff7fbfa059bf26c84ddb80 with
x0,
V_ x1 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_a2c3fca2e8c461af2fcd2014916bc97ec486da998a233beedf90ec14d6bf2e76 with
x0,
x3,
x1 leaving 2 subgoals.
The subproof is completed by applying H3.
Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
x0,
V_ x3.
Let x4 of type ι be given.
Apply unknownprop_75b5762e65badae8f9531d40fddd332ff95b59f608d93c7a55f19f4fa5ef37d5 with
x4,
V_ x3.
Assume H7:
nIn x4 (V_ x3).
Apply notE with
∃ x5 . and (In x5 x0) (nIn x5 (V_ x3)) leaving 2 subgoals.
The subproof is completed by applying H5.
Let x5 of type ο be given.
Assume H8:
∀ x6 . and (In x6 x0) (nIn x6 (V_ x3)) ⟶ x5.
Apply H8 with
x4.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
In x4 x0,
nIn x4 (V_ x3) leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
Apply L5 with
In x2 (V_ x0).
Let x4 of type ι be given.
Assume H6:
(λ x5 . and (In x5 x0) (nIn x5 (V_ x3))) x4.
Apply andE with
In x4 x0,
nIn x4 (V_ x3),
In x2 (V_ x0) leaving 2 subgoals.
The subproof is completed by applying H6.
Assume H8:
nIn x4 (V_ x3).
Apply unknownprop_eb8e8f72a91f1b934993d4cb19c84c8270f73a3626f3022b683d960a7fef89cb with
In x4 (V_ x3),
Subq (V_ x3) (V_ x4),
In x2 (V_ x0) leaving 3 subgoals.
Apply H0 with
x4,
x3.
The subproof is completed by applying H7.
Assume H9:
In x4 (V_ x3).
Apply FalseE with
In x2 (V_ x0).
Apply unknownprop_8369708f37c0d20e10b6156293f1b207e835dfc563ff7fbfa059bf26c84ddb80 with
x4,
V_ x3 leaving 2 subgoals.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
Apply unknownprop_16d2e0ac4e61f9d6f4710f68fd29bc0751fdb2a43ae4ee41dc39565d6502f8a7 with
x2,
V_ x3,
V_ x4 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H9.
Apply unknownprop_a2c3fca2e8c461af2fcd2014916bc97ec486da998a233beedf90ec14d6bf2e76 with
x2,
x4,
x0 leaving 2 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying L10.