Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_a11dfa210cd480918339ec3ee480411b7f4945c0aeef474c01ca879d15816c74 with
bc82c.. (ce322.. x0) (ce322.. x1),
bc82c.. (f6a32.. x0) (f6a32.. x1) leaving 2 subgoals.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with
ce322.. x0,
ce322.. x1 leaving 2 subgoals.
Apply unknownprop_c50e383ae63caacff66491342f6a1cc504e440cc936d7430270036bd6758f48a with
x0.
The subproof is completed by applying H0.
Apply unknownprop_c50e383ae63caacff66491342f6a1cc504e440cc936d7430270036bd6758f48a with
x1.
The subproof is completed by applying H1.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with
f6a32.. x0,
f6a32.. x1 leaving 2 subgoals.
Apply unknownprop_29514e25826fa0a942e92f047f92b24dd63fba7537353bf59d9f591e0be2370c with
x0.
The subproof is completed by applying H0.
Apply unknownprop_29514e25826fa0a942e92f047f92b24dd63fba7537353bf59d9f591e0be2370c with
x1.
The subproof is completed by applying H1.