Proofgold Proof

pf

Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H0: prim0 x0 x1 = prim0 x2 x3.

Apply unknownprop_f4ff16b9b21fb43bec0dd0d2e94569d632f3d21b75932b9bcc0c1ffd4c0d62b6 with x0, x1, x2, x3, x0 = x2 leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H1: x0 = x2.

Assume H2: x1 = x3.

The subproof is completed by applying H1.

■