Proofgold Proof

pf

Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: SNo x0.

Assume H1: ∀ x3 . x3 ∈ SNoS_ (SNoLev x0) ⟶ ∀ x4 x5 . SNoCutP x4 x5 ⟶ x3 = SNoCut x4 x5 ⟶ minus_SNo x3 = SNoCut (prim5 x5 minus_SNo) (prim5 x4 minus_SNo).

Assume H2: SNoCutP x1 x2.

Assume H3: ∀ x3 . x3 ∈ x2 ⟶ SNo x3.

Assume H4: x0 = SNoCut x1 x2.

Assume H5: SNo (SNoCut x1 x2).

Apply H4 with λ x3 x4 . minus_SNo x4 = SNoCut (prim5 x2 minus_SNo) (prim5 x1 minus_SNo).

Apply minus_SNoCut_eq with x1, x2.

The subproof is completed by applying H2.

■