Let x0 of type ι → (ι → ι → ι) → (ι → ι) → ι → ι → ο be given.
Let x1 of type ι be given.
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 H0:
∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x2 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι . (∀ x8 . prim1 x8 x1 ⟶ x3 x8 = x7 x8) ⟶ x0 x1 x6 x7 x4 x5 = x0 x1 x2 x3 x4 x5.
Apply unknownprop_0663073412d695176e3e23ffbbbb5da2857252d5c0f47051c9f0c33ecb11f4b6 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x6 (e3162.. (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4 x5.
Apply unknownprop_a5be19faa2e80b8da858086292146d3f609318d0df557aec5c9ce5a6ab6b4ab0 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x1 (e3162.. (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4 x5.
Apply unknownprop_c1003d86b72ccf1c88f05bbb3160c1287244e653b755f6f0f8f6e6dea303f1e4 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x1 (e3162.. (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x6 = x0 x1 x2 x3 x4 x5.
Apply H0 with
e3162.. (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)),
f482f.. (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))) leaving 2 subgoals.
The subproof is completed by applying unknownprop_a0d932da53985136bc4d111609d0ae5a2ed2e4f1789b9bd8811552fd687d1136 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_c64bca701150bd7d152f116af6a1108b34c2b6e6d2765f2dada41711a2cb9dfa with x1, x2, x3, x4, x5.