Let x0 of type ι be given.
Apply unknownprop_fa66e3d1737b2c05fa4008399b4c740ee88bf9334c6b435957b41684dfedfe51 with
1ad11.. x0 x0.
Let x1 of type ι be given.
Apply unknownprop_564070ebbc5072b968224a9385fce4a5357a5716df4a6e9af28a2476cbfa8a7d with
x0,
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_f3a4771d3d9a8514b2ad16b328a764b0ce93421ae4df5a6923d3e167d035e33a with
x0,
x0,
x1.
The subproof is completed by applying H0.