Proofgold Proof

pf

Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: SNoCutP x0 x1.

Apply minus_SNoCut_eq_lem with SNoCut x0 x1, x0, x1 leaving 3 subgoals.

Apply SNoCutP_SNo_SNoCut with x0, x1.

The subproof is completed by applying H0.

The subproof is completed by applying H0.

Let x2 of type ι → ι → ο be given.

Assume H1: x2 (SNoCut x0 x1) (SNoCut x0 x1).

The subproof is completed by applying H1.

■