Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_f97432d9e47c0e51520ba4c55aa341901f6387f434845746cd842c12e77717b7 with
x0,
x1,
f4dc0.. x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_8fbd0c2b48e78882e15936a0ad5f4a3c5af2cb37d9320d8cb210a91462e202ca with
x2.
The subproof is completed by applying H2.