Let x0 of type ι be given.
Apply unknownprop_a3a7565e6ec36921ef8d95ac6064e5fb0324fd3fb8dbfeef6aeadeb5800cae4a with
λ x1 x2 : ι → ο . x2 x0 ⟶ ∀ x3 . In x3 x0 ⟶ In (ordsucc x3) (ordsucc x0).
Assume H0:
(λ x1 . ∀ x2 : ι → ο . x2 0 ⟶ (∀ x3 . x2 x3 ⟶ x2 (ordsucc x3)) ⟶ x2 x1) x0.
Apply H0 with
λ x1 . ∀ x2 . In x2 x1 ⟶ In (ordsucc x2) (ordsucc x1) leaving 2 subgoals.
Let x1 of type ι be given.
Apply FalseE with
In (ordsucc x1) 1.
Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with
x1.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_84fe37a922385756a4e0826a593defb788cadbe4bdc9a7fe6b519ea49f509df5 with
x1,
x2,
In (ordsucc x2) (ordsucc (ordsucc x1)) leaving 3 subgoals.
The subproof is completed by applying H2.
Apply H1 with
x2.
The subproof is completed by applying H3.
Apply unknownprop_9d1f2833af10907d78259d2045ff2d1e1026643f459cca4199c4ae7f89385ba4 with
ordsucc x1,
ordsucc x2.
The subproof is completed by applying L4.
Assume H3: x2 = x1.
Apply H3 with
λ x3 x4 . In (ordsucc x4) (ordsucc (ordsucc x1)).
The subproof is completed by applying unknownprop_4b3850b342b3607d712ced4e4c9fa37dbdc70692760e3dc82f8fd86e9b26a6b5 with
ordsucc x1.