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 ⟶ ∀ x9 . prim1 x9 x1 ⟶ x3 x8 x9 = x7 x8 x9) ⟶ x0 x1 x6 x7 x4 x5 = x0 x1 x2 x3 x4 x5.
Apply unknownprop_6f39622dc76232e085e721e3af2c53ec3999921c69ca138ff988a417c031d4d3 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x6 (e3162.. (f482f.. (c77b5.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (c77b5.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (c77b5.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (c77b5.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4 x5.
Apply unknownprop_57ed960db242abdef6ccb4e85d7c3fe84854d10784c2f6652f9e93c7eddc75f1 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x1 (e3162.. (f482f.. (c77b5.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (c77b5.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (f482f.. (c77b5.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4 x5.
Apply unknownprop_d017dec9cdb5f9f4826d233a0253fa01a4b0d4f422a1a13928abbd3f018080a0 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x1 (e3162.. (f482f.. (c77b5.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (c77b5.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x6 = x0 x1 x2 x3 x4 x5.
Apply H0 with
e3162.. (f482f.. (c77b5.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)),
e3162.. (f482f.. (c77b5.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))) leaving 2 subgoals.
The subproof is completed by applying unknownprop_060a246b383448729e9ee5f39cb39f8718fb6c0d19e2f23c23ee11958bbba2a7 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_f8fac6001579932f99322d02801fcfcbf2ebfe75de5be6a1c0b22de9632a3f27 with x1, x2, x3, x4, x5.