Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: SNo x0.

Assume H1: SNo x1.

Assume H2: PNoLe (SNoLev x0) (λ x2 . x2 ∈ x0) (SNoLev x1) (λ x2 . x2 ∈ x1).

Apply H2 with or (SNoLt x0 x1) (x0 = x1) leaving 2 subgoals.

Assume H3: PNoLt (SNoLev x0) (λ x2 . x2 ∈ x0) (SNoLev x1) (λ x2 . x2 ∈ x1).

Apply orIL with SNoLt x0 x1, x0 = x1.

The subproof is completed by applying H3.

Assume H3: and (SNoLev x0 = SNoLev x1) (PNoEq_ (SNoLev x0) (λ x2 . x2 ∈ x0) (λ x2 . x2 ∈ x1)).

Apply H3 with or (SNoLt x0 x1) (x0 = x1).

Assume H4: SNoLev x0 = SNoLev x1.

Assume H5: PNoEq_ (SNoLev x0) (λ x2 . x2 ∈ x0) (λ x2 . x2 ∈ x1).

Apply orIR with SNoLt x0 x1, x0 = x1.

Apply SNo_eq with x0, x1 leaving 4 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

The subproof is completed by applying H4.

The subproof is completed by applying H5.

■

Proofgold Proof