Let x0 of type ι → (ι → ο) → ο be given.
Let x1 of type ι → (ι → ο) → ο be given.
Let x2 of type ι be given.
Apply unknownprop_6419f8fc1ff70ca950cf4e79a0f0cff9b9f9b876ea55c76aec20f2ed9adc5971 with
x0,
x1,
x2,
prim1 (7b9f3.. x0 x1) (4ae4a.. x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply H4 with
(∀ x3 . prim1 x3 (7b9f3.. x0 x1) ⟶ ∀ x4 : ι → ο . not (47618.. x0 x1 x3 x4)) ⟶ prim1 (7b9f3.. x0 x1) (4ae4a.. x2).
Apply unknownprop_13deec40494b47380fd1941c6a625d447cd8171018141d4d3bc740ca96c35ef7 with
x0,
x1,
x2,
prim1 (7b9f3.. x0 x1) (4ae4a.. x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Let x3 of type ι be given.
Apply H8 with
prim1 (7b9f3.. x0 x1) (4ae4a.. x2).
Assume H10:
∃ x4 : ι → ο . 47618.. x0 x1 x3 x4.
Apply H10 with
prim1 (7b9f3.. x0 x1) (4ae4a.. x2).
Let x4 of type ι → ο be given.
Apply unknownprop_1f03c3e4cc230143731a84d6351b78522f6051d5113f644774435abf9cb5a984 with
x2.
The subproof is completed by applying H1.
Apply ordinal_In_Or_Subq with
7b9f3.. x0 x1,
4ae4a.. x2,
prim1 (7b9f3.. x0 x1) (4ae4a.. x2) leaving 4 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying L12.
The subproof is completed by applying H13.
Apply FalseE with
prim1 (7b9f3.. x0 x1) (4ae4a.. x2).
Apply H13 with
x3.
The subproof is completed by applying H9.
Apply H7 with
x3,
x4 leaving 2 subgoals.
The subproof is completed by applying L14.
The subproof is completed by applying H11.