Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_f82d0f217e1b2a36bc273d145ee21e9b9e753d654bb0c650cc08860c1b4bd1f0 with
x0,
x1,
equip x0 x2 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x3 of type ι → ι be given.
Apply unknownprop_f82d0f217e1b2a36bc273d145ee21e9b9e753d654bb0c650cc08860c1b4bd1f0 with
x1,
x2,
equip x0 x2 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x4 of type ι → ι be given.
Apply unknownprop_4b95783dcb3eee1943e1de5542f675166ef402c8fbdda80bdf0920b55d3fc6de with
x0,
x2,
λ x5 . x4 (x3 x5).
Apply unknownprop_cb9a1666f1bb680609161999e9252fab563daa1c313191fba56ade1e24f1f047 with
x0,
x1,
x2,
x3,
x4 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.