Let x0 of type ι be given.
Apply unknownprop_4865425a7f56150b37062def658749568c73ac3811495e4e2624803c98cf736b with
b5c9f.. (4ae4a.. (4ae4a.. 4a7ef..)) x0,
e5b72.. x0,
λ x1 . 1216a.. x0 (λ x2 . f482f.. x1 x2 = 4ae4a.. 4a7ef..).
Apply and3I with
∀ x1 . prim1 x1 (b5c9f.. (4ae4a.. (4ae4a.. 4a7ef..)) x0) ⟶ prim1 ((λ x2 . 1216a.. x0 (λ x3 . f482f.. x2 x3 = 4ae4a.. 4a7ef..)) x1) (e5b72.. x0),
∀ x1 . prim1 x1 (b5c9f.. (4ae4a.. (4ae4a.. 4a7ef..)) x0) ⟶ ∀ x2 . prim1 x2 (b5c9f.. (4ae4a.. (4ae4a.. 4a7ef..)) x0) ⟶ (λ x3 . 1216a.. x0 (λ x4 . f482f.. x3 x4 = 4ae4a.. 4a7ef..)) x1 = (λ x3 . 1216a.. x0 (λ x4 . f482f.. x3 x4 = 4ae4a.. 4a7ef..)) x2 ⟶ x1 = x2,
∀ x1 . prim1 x1 (e5b72.. x0) ⟶ ∃ x2 . and (prim1 x2 (b5c9f.. (4ae4a.. (4ae4a.. 4a7ef..)) x0)) ((λ x3 . 1216a.. x0 (λ x4 . f482f.. x3 x4 = 4ae4a.. 4a7ef..)) x2 = x1) leaving 3 subgoals.
Let x1 of type ι be given.
The subproof is completed by applying unknownprop_04c97c2c2d1a8e1962ff0429ce82d65b677812398d5dd7ead59c810d35c83fce with
x0,
λ x2 . f482f.. x1 x2 = 4ae4a.. 4a7ef...
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_37fcf738b3aad2297378a2358f205c1613763d36e48c6969ecd725fbc7fdfb27 with
x0,
λ x3 . 4ae4a.. (4ae4a.. 4a7ef..),
x1,
x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Let x3 of type ι be given.
Apply unknownprop_285d1412c16abfd3320f0ee89e600fad3199271183754290c3d7bd1f86d5a491 with
f482f.. x1 x3,
λ x4 . f482f.. x1 x3 = x4 ⟶ f482f.. x1 x3 = f482f.. x2 x3 leaving 4 subgoals.
The subproof is completed by applying L4.
Apply unknownprop_285d1412c16abfd3320f0ee89e600fad3199271183754290c3d7bd1f86d5a491 with
f482f.. x2 x3,
λ x4 . f482f.. x2 x3 = x4 ⟶ f482f.. x1 x3 = f482f.. x2 x3 leaving 4 subgoals.
The subproof is completed by applying L5.
Claim L8: ∀ x6 : ι → ο . x6 y5 ⟶ x6 y4
Let x6 of type ι → ο be given.
Apply H6 with
λ x7 . x6.
set y7 to be λ x7 . x6
Apply H7 with
λ x8 x9 . y7 x9 x8.
The subproof is completed by applying H8.
Let x6 of type ι → ι → ο be given.
Apply L8 with
λ x7 . x6 x7 y5 ⟶ x6 y5 x7.
Assume H9: x6 y5 y5.
The subproof is completed by applying H9.