Let x0 of type ι → ι be given.
Apply unknownprop_ea78574cb3264467ecb0cee6dab0f2cbbdf0e0a00f843238d57e1be6acdbe25f with
a842e.. 4a7ef.. (λ x1 . x0 x1).
Let x1 of type ι be given.
Apply unknownprop_a49caa60ea4ba8fae09092811c2c569b8a372e604c938e38dc3c1566f7ef2d14 with
4a7ef..,
x0,
x1,
prim1 x1 4a7ef.. leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Apply FalseE with
prim1 x1 (x0 x2) ⟶ prim1 x1 4a7ef...
Apply unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with
x2.
The subproof is completed by applying H1.