Proofgold Proof

pf

Let x0 of type ι be given.

Assume H0: not (empty_p x0).

Let x1 of type ι be given.

Assume H1: 4326e.. x0 x1.

Apply H1 with prim1 x1 x0 leaving 2 subgoals.

Assume H2: prim1 x1 x0.

The subproof is completed by applying H2.

Assume H2: and (empty_p x0) (empty_p x1).

Apply H2 with prim1 x1 x0.

Assume H3: empty_p x0.

Apply FalseE with empty_p x1 ⟶ prim1 x1 x0.

Apply H0.

The subproof is completed by applying H3.

■