Proofgold Proof

pf

Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: Subq x2 x0.

Assume H1: Subq x2 x1.

Let x3 of type ι be given.

Assume H2: prim1 x3 x2.

Apply unknownprop_0eb2245dc687a56a5adef9ad3fc675715803356fcfbd14168f93f22b67fac4c1 with x0, x1, x3 leaving 2 subgoals.

Apply H0 with x3.

The subproof is completed by applying H2.

Apply H1 with x3.

The subproof is completed by applying H2.

■