Let x0 of type ι → (ι → ο) → ο be given.
Let x1 of type ι be given.
Let x2 of type ι → ο be given.
Let x3 of type ι be given.
Apply H0 with
6f2c4.. x0 x1 x2 ⟶ 6f2c4.. x0 x3 x2.
Apply ordinal_Hered with
x1,
x3 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply L4 with
TransSet x3.
The subproof is completed by applying H5.
Let x4 of type ι be given.
Let x5 of type ι → ο be given.
Apply H2 with
x3,
x4 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H7.
Apply H6 with
x4,
x5 leaving 2 subgoals.
The subproof is completed by applying L9.
The subproof is completed by applying H8.
Apply unknownprop_1c12738cd89f8c615a541c15b6797bba2a5be97ab5e514c9fd76b3fef06e2aa9 with
x4,
x1,
x5,
x2,
40dde.. x4 x5 x3 x2 leaving 4 subgoals.
The subproof is completed by applying L10.
Apply unknownprop_71c983f9883b4f28b7b9554926463bb4627a33e675a17eaba24400b257e59781 with
x4,
x1.
Apply H2 with
x4.
The subproof is completed by applying L9.
Apply unknownprop_71c983f9883b4f28b7b9554926463bb4627a33e675a17eaba24400b257e59781 with
x4,
x3.
Apply L5 with
x4.
The subproof is completed by applying H7.
Apply unknownprop_ac970f51deca19d20e9a8350c3518ea802533ebd2768fe799c9b97ea3dd03596 with
x4,
x3,
x5,
x2.
Apply L13 with
λ x6 x7 . PNoLt_ x7 x5 x2.
Apply L12 with
λ x6 x7 . PNoLt_ x6 x5 x2.
The subproof is completed by applying H11.
Assume H13: x2 x4.
Apply unknownprop_9bcd3ca68066c7069c00444b0b53fe3ae6267cb29974000b72e5fe8327360c0b with
x4,
x3,
x5,
x2 leaving 3 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H12.
The subproof is completed by applying H13.
Apply FalseE with
PNoEq_ x1 x5 x2 ⟶ not (x5 x1) ⟶ 40dde.. x4 x5 x3 x2.
Apply unknownprop_f1a526a64fd91875cd825eea7f2e7776b7f0e7be5dcee74dc03af1d7886d1eb6 with
x1,
x4 leaving 2 subgoals.
The subproof is completed by applying H11.
The subproof is completed by applying L9.