Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_d74508268cf2245bb4de852843c85bf4733bd48f6383eaac9c68dfae0d149115 with
x0,
x1.
Let x2 of type ι be given.
Apply iffI with
prim1 x2 x0,
prim1 x2 x1 leaving 2 subgoals.
The subproof is completed by applying H0 with x2.
The subproof is completed by applying H1 with x2.