Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply unknownprop_f4ff16b9b21fb43bec0dd0d2e94569d632f3d21b75932b9bcc0c1ffd4c0d62b6 with
236c6..,
prim0 x0 x1,
236c6..,
prim0 x2 x3,
∀ x4 : ο . (x0 = x2 ⟶ x1 = x3 ⟶ x4) ⟶ x4 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_f4ff16b9b21fb43bec0dd0d2e94569d632f3d21b75932b9bcc0c1ffd4c0d62b6 with x0, x1, x2, x3.