Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_a90cef7a0ba9512cc0d2e629e580894b6ddc586580e86ce1ae226da918648109 with
x1.
Apply unknownprop_d85f3547e44aa37ab9cec732e4a27c75688e02eb3cb6e8c94c8a00b324e73b36 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.