Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_f82d0f217e1b2a36bc273d145ee21e9b9e753d654bb0c650cc08860c1b4bd1f0 with
x0,
x1,
equip x1 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι → ι be given.
Apply unknownprop_4b95783dcb3eee1943e1de5542f675166ef402c8fbdda80bdf0920b55d3fc6de with
x1,
x0,
ed93b.. x0 x2.
Apply unknownprop_e3addc904303a6dbb15774354394f657dd4adceaefafc059eea14906492d8def with
x0,
x1,
x2.
The subproof is completed by applying H1.