Let x0 of type (ι → ι) → ο be given.
Let x1 of type ι be given.
Claim L1:
(λ x2 . ∀ x3 : ι → ι . x0 x3 ⟶ x3 x2 = x3 x1) = λ x2 . ∀ x3 : ι → ι . x0 x3 ⟶ x3 x2 = x3 (fa4ab.. x0 (λ x4 : ι → ι . x4 x1))Apply functional extensionality with
λ x2 . ∀ x3 : ι → ι . x0 x3 ⟶ x3 x2 = x3 x1,
λ x2 . ∀ x3 : ι → ι . x0 x3 ⟶ x3 x2 = x3 (fa4ab.. x0 (λ x4 : ι → ι . x4 x1)).
Let x2 of type ι be given.
Apply prop_ext_2 with
∀ x3 : ι → ι . x0 x3 ⟶ x3 x2 = x3 x1,
∀ x3 : ι → ι . x0 x3 ⟶ x3 x2 = x3 (fa4ab.. x0 (λ x4 : ι → ι . x4 x1)) leaving 2 subgoals.
Assume H1: ∀ x3 : ι → ι . x0 x3 ⟶ x3 x2 = x3 x1.
Let x3 of type ι → ι be given.
Assume H2: x0 x3.
Apply H1 with
x3,
λ x4 x5 . x5 = x3 (fa4ab.. x0 (λ x6 : ι → ι . x6 x1)) leaving 2 subgoals.
The subproof is completed by applying H2.
Claim L3:
x3 (fa4ab.. x0 (λ x4 : ι → ι . x4 x1)) = x3 x1Apply unknownprop_00aa39c102a7496c4eb368cb49342e9cbd91fecf464438f3bb170319c186ca5f with
x0,
x3,
λ x4 : ι → ι . x4 x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Let x4 of type ι → ι → ο be given.
The subproof is completed by applying L3 with λ x5 x6 . x4 x6 x5.
Assume H1:
∀ x3 : ι → ι . x0 x3 ⟶ x3 x2 = x3 (fa4ab.. x0 (λ x4 : ι → ι . x4 x1)).
Let x3 of type ι → ι be given.
Assume H2: x0 x3.
Apply H1 with
x3,
λ x4 x5 . x5 = x3 x1 leaving 2 subgoals.
The subproof is completed by applying H2.
Apply unknownprop_00aa39c102a7496c4eb368cb49342e9cbd91fecf464438f3bb170319c186ca5f with
x0,
x3,
λ x4 : ι → ι . x4 x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply L1 with
λ x2 x3 : ι → ο . prim0 x3 = prim0 (λ x4 . ∀ x5 : ι → ι . x0 x5 ⟶ x5 x4 = x5 (fa4ab.. x0 (λ x6 : ι → ι . x6 x1))).
Let x2 of type ι → ι → ο be given.
Assume H2:
x2 (prim0 (λ x3 . ∀ x4 : ι → ι . x0 x4 ⟶ x4 x3 = x4 (fa4ab.. x0 (λ x5 : ι → ι . x5 x1)))) (prim0 (λ x3 . ∀ x4 : ι → ι . x0 x4 ⟶ x4 x3 = x4 (fa4ab.. x0 (λ x5 : ι → ι . x5 x1)))).
The subproof is completed by applying H2.