Let x0 of type ι → ι → ο be given.
Apply unknownprop_5574bdb5e5df6f14031f4de95b01de091bd6680b3f0f837fce12fa18146d5760 with
x0,
∀ x1 x2 . combinator_equiv x1 x2 ⟶ x0 x1 x2 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_6d861aa069d3c6b52ea4a1626e236a28ccef38ff01ec7a48d612e144c66b13b6 with
λ x3 x4 : ι → ι → ο . x4 x1 x2 ⟶ x0 x1 x2.
Apply H7 with
λ x3 x4 . and (combinator_equiv x3 x4) (x0 x3 x4) leaving 5 subgoals.
Apply unknownprop_3c590cab2ff9c9cfe8b972f88872dc13917f1366b105f7b06fc323fa84f097bb with
λ x3 x4 . and (combinator_equiv x3 x4) (x0 x3 x4) leaving 2 subgoals.
Apply unknownprop_aec34b0d0cf76dca91d048e65b0ba169e2aa775687c2b9251cda71d8c85d19d1 with
λ x3 x4 . and (combinator_equiv x3 x4) (x0 x3 x4).
Let x3 of type ι be given.
Let x4 of type ι be given.
Apply unknownprop_896ccc9f209efa8a895211d65adb5a90348b419f100f6ab5e9762ce4d7fa9cc1 with
combinator_equiv x1 x2,
x0 x1 x2.
The subproof is completed by applying L8.