Claim L0:
∀ x0 . ∀ x1 : ο . (∀ x2 . nat_p x2 ⟶ Subq x0 (V_ x2) ⟶ x1) ⟶ x1Apply unknownprop_39a49b81f8178fc2503c8c110411db8e10126354e93190c5742776bc6d7f1d90 with
λ x0 . ∀ x1 : ο . (∀ x2 . nat_p x2 ⟶ Subq x0 (V_ x2) ⟶ x1) ⟶ x1 leaving 5 subgoals.
Let x0 of type ι be given.
Assume H0:
(λ x1 . ∀ x2 : ο . (∀ x3 . nat_p x3 ⟶ Subq x1 (V_ x3) ⟶ x2) ⟶ x2) x0.
Let x1 of type ι be given.
Let x2 of type ο be given.
Apply H0 with
x2.
Let x3 of type ι be given.
Apply H2 with
x3 leaving 2 subgoals.
The subproof is completed by applying H3.
Apply unknownprop_5af24edc592c6d7fa3cf53e40211635bbed8f39380469ac8aef3490ee700739c with
V_ x3,
x1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_246dbbaa90a30a59bb82c977db3a76b865348aa516921f45ddd5a06925460ee4 with x3.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with
x0,
V_ x3,
x1 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H1.
Let x0 of type ο be given.
Apply H0 with
0 leaving 2 subgoals.
The subproof is completed by applying unknownprop_0e150139fedb8d7a0ae85e3054b4c73c936e7acb880ce730fb00a0093c9c6c27.
Apply unknownprop_fa1d3a4a00c90be7720377aeb98583e9ec1104c7f9b8661e216ae25581a1e970 with
λ x1 x2 . Subq 0 x2.
The subproof is completed by applying unknownprop_d889823a5c975ad2d68f484964233a1e69e7d67f0888aa5b83d962eeca107acd with 0.
Let x0 of type ι be given.
Assume H0:
(λ x1 . ∀ x2 : ο . (∀ x3 . nat_p x3 ⟶ Subq x1 (V_ x3) ⟶ x2) ⟶ x2) x0.
Let x1 of type ο be given.
Apply H0 with
x1.
Let x2 of type ι be given.
Apply H1 with
x2 leaving 2 subgoals.
The subproof is completed by applying H2.
Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
Union x0,
V_ x2.
Let x3 of type ι be given.
Apply unknownprop_99c6830b7507eb1c538c7366f637e956be6dad337531dd2702ca6ba6923a9849 with
x0,
x3,
In x3 (V_ x2) leaving 2 subgoals.
The subproof is completed by applying H4.
Let x4 of type ι be given.
Apply unknownprop_5af24edc592c6d7fa3cf53e40211635bbed8f39380469ac8aef3490ee700739c with
V_ x2,
x4 leaving 2 subgoals.
The subproof is completed by applying unknownprop_246dbbaa90a30a59bb82c977db3a76b865348aa516921f45ddd5a06925460ee4 with x2.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with
x0,
V_ x2,
x4 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H6.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with
x4,
V_ x2,
x3 leaving 2 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying H5.
Let x0 of type ι be given.
Assume H0:
(λ x1 . ∀ x2 : ο . (∀ x3 . nat_p x3 ⟶ Subq x1 (V_ x3) ⟶ x2) ⟶ x2) x0.
Let x1 of type ο be given.
Apply H0 with
x1.
Let x2 of type ι be given.
Apply H1 with
ordsucc x2 leaving 2 subgoals.
Apply unknownprop_077979b790f9097ea9250573e60509ec9410103c35a67e0558983ee18582fb09 with
x2.
The subproof is completed by applying H2.
Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
Power x0,
V_ (ordsucc x2).
Let x3 of type ι be given.
Apply unknownprop_a2c3fca2e8c461af2fcd2014916bc97ec486da998a233beedf90ec14d6bf2e76 with
x3,
x2,
ordsucc x2 leaving 2 subgoals.
The subproof is completed by applying unknownprop_4b3850b342b3607d712ced4e4c9fa37dbdc70692760e3dc82f8fd86e9b26a6b5 with x2.
Apply unknownprop_16d2e0ac4e61f9d6f4710f68fd29bc0751fdb2a43ae4ee41dc39565d6502f8a7 with
...,
...,
... leaving 2 subgoals.
Let x0 of type ι be given.
Apply L0 with
x0,
∃ x1 . and (nat_p x1) (Subq x0 (V_ x1)).
Let x1 of type ι be given.
Let x2 of type ο be given.
Apply H3 with
x1.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
nat_p x1,
Subq x0 (V_ x1) leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.