Let x0 of type ι → ι → ο be given.
Apply ordinal_ind with
λ x1 . ∀ x2 . ordinal x2 ⟶ ∀ x3 . prim1 x3 (56ded.. x1) ⟶ ∀ x4 . prim1 x4 (56ded.. x2) ⟶ x0 x3 x4.
Let x1 of type ι be given.
Apply ordinal_ind with
λ x2 . ∀ x3 . prim1 x3 (56ded.. x1) ⟶ ∀ x4 . prim1 x4 (56ded.. x2) ⟶ x0 x3 x4.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Apply unknownprop_cd21c13b2c3f5b1a3b98367fcb2ef0b03b319d8c325362ea48d721c1e2e4842f with
x1,
x3,
x0 x3 x4 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H5.
Apply unknownprop_cd21c13b2c3f5b1a3b98367fcb2ef0b03b319d8c325362ea48d721c1e2e4842f with
x2,
x4,
x0 x3 x4 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H6.
Apply H0 with
x3,
x4 leaving 5 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying H13.
Let x5 of type ι be given.
Apply H2 with
e4431.. x3,
x2,
x5,
x4 leaving 4 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H3.
The subproof is completed by applying H15.
The subproof is completed by applying H6.
Apply H4 with
e4431.. x4,
x3 leaving 2 subgoals.
The subproof is completed by applying H11.
The subproof is completed by applying H5.
Let x5 of type ι be given.
Let x6 of type ι be given.
Apply H2 with
e4431.. x3,
e4431.. x4,
x5,
x6 leaving 4 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H12.
The subproof is completed by applying H15.
The subproof is completed by applying H16.
Apply unknownprop_800ab0f9f7d5e23ffc560fa6f3a77275d4dd8d39b4817caedaa494e089e82bfc with
x0.
The subproof is completed by applying L1.