Proofgold Proof

pf
Let x0 of type ι be given. Let x1 of type ι be given. Assume H0: ∀ x2 . x2 ∈ x0 ⟶ minus_SNo (minus_SNo x2) = x2. Assume H1: ∀ x2 . x2 ∈ x1 ⟶ minus_SNo (minus_SNo x2) = x2. Assume H2: ∀ x2 . x2 ∈ x0 ⟶ SNo x2. Assume H3: ∀ x2 . x2 ∈ x1 ⟶ SNo x2. The subproof is completed by applying minus_SNo_invol with SNoCut x0 x1. ■