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