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