Let x0 of type ι → ο be given.
Let x1 of type (ι → ι) → ο be given.
Assume H0: ∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3).
Assume H1: ∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4).
Let x2 of type ι → ι be given.
Let x3 of type ι → ι be given.
Let x4 of type ι → ι be given.
Let x5 of type ι → ι be given.
Assume H2: x1 x2.
Assume H3: x1 x3.
Assume H4: x1 x4.
Assume H5: x1 x5.
Let x6 of type ι be given.
Assume H6: x0 x6.
Apply unknownprop_83a891a4a926cbdce37fd271221fb0ce58c8a724c37c2abb7450afddc5f40841 with
x0,
x1,
x3,
x4,
x5,
x6,
λ x7 x8 . x2 x8 = x5 (x2 (x3 (x4 x6))) leaving 7 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
Apply unknownprop_89fd83854c5f1d85e8a25a695cd9584e2107dbdc7c3e9ce5049e96e430f178b4 with
x0,
x1,
x2,
x5,
x3,
x4,
x6 leaving 7 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 H5.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H6.