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