Let x0 of type ι → ο be given.
Assume H0: x0 0.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
nat_p 0,
x0 0 leaving 2 subgoals.
The subproof is completed by applying unknownprop_0e150139fedb8d7a0ae85e3054b4c73c936e7acb880ce730fb00a0093c9c6c27.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Apply andE with
nat_p x1,
x0 x1,
and (nat_p (ordsucc x1)) (x0 (ordsucc x1)) leaving 2 subgoals.
The subproof is completed by applying H3.
Assume H5: x0 x1.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
nat_p (ordsucc x1),
x0 (ordsucc x1) leaving 2 subgoals.
Apply unknownprop_077979b790f9097ea9250573e60509ec9410103c35a67e0558983ee18582fb09 with
x1.
The subproof is completed by applying H4.
Apply H1 with
x1 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Let x1 of type ι be given.
Apply unknownprop_a3a7565e6ec36921ef8d95ac6064e5fb0324fd3fb8dbfeef6aeadeb5800cae4a with
λ x2 x3 : ι → ο . x3 x1 ⟶ x0 x1.
Assume H4:
(λ x2 . ∀ x3 : ι → ο . x3 0 ⟶ (∀ x4 . x3 x4 ⟶ x3 (ordsucc x4)) ⟶ x3 x2) x1.
Apply H4 with
λ x2 . and (nat_p x2) (x0 x2) leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
Apply unknownprop_896ccc9f209efa8a895211d65adb5a90348b419f100f6ab5e9762ce4d7fa9cc1 with
nat_p x1,
x0 x1.
The subproof is completed by applying L5.