Let x0 of type ι → ι be given.
Apply unknownprop_fa66e3d1737b2c05fa4008399b4c740ee88bf9334c6b435957b41684dfedfe51 with
94f9e.. 4a7ef.. (λ x1 . x0 x1).
Let x1 of type ι be given.
Apply unknownprop_d908b89102f7b662c739e5a844f67efc8ae1cd05a2e9ce1e3546fa3885f40100 with
4a7ef..,
x0,
x1,
False leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Assume H2: x1 = x0 x2.
Apply unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with
x2.
The subproof is completed by applying H1.