Let x0 of type ι be given.
Apply unknownprop_dfa3c3c24a3fb387a38cf914eae39660043652084cee67961f4d3cf4eccb0c62 with
x0,
λ x1 . ∀ x2 . In x2 x1 ⟶ ∀ x3 : ι → ο . (∀ x4 . nat_p x4 ⟶ x1 = ordsucc x4 ⟶ x3 (ordsucc x4)) ⟶ x3 x1 leaving 3 subgoals.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Apply FalseE with
∀ x2 : ι → ο . (∀ x3 . nat_p x3 ⟶ 0 = ordsucc x3 ⟶ x2 (ordsucc x3)) ⟶ x2 0.
Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with
x1.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι → ο be given.
Apply H2 with
λ x4 x5 . (∀ x6 . nat_p x6 ⟶ x4 = ordsucc x6 ⟶ x3 (ordsucc x6)) ⟶ x3 (ordsucc x1).
Apply H4 with
x1 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.