Apply SNoLev_ind with λ x0 . add_SNo 0 x0 = x0.

Let x0 of type ι be given.

Assume H0: SNo x0.

Assume H1: ∀ x1 . x1 ∈ SNoS_ (SNoLev x0) ⟶ add_SNo 0 x1 = x1.

Apply add_SNo_eq with 0, x0, λ x1 x2 . x2 = x0 leaving 3 subgoals.

The subproof is completed by applying SNo_0.

The subproof is completed by applying H0.

Claim L2: binunion {add_SNo x1 x0|x1 ∈ SNoL 0} {add_SNo 0 x1|x1 ∈ SNoL x0} = SNoL x0

Apply SNoL_0 with λ x1 x2 . binunion {add_SNo x3 x0|x3 ∈ x2} {add_SNo 0 x3|x3 ∈ SNoL x0} = SNoL x0.

Apply Repl_Empty with λ x1 . add_SNo x1 x0, λ x1 x2 . binunion x2 {add_SNo 0 x3|x3 ∈ SNoL x0} = SNoL x0.

Apply binunion_idl with {add_SNo 0 x1|x1 ∈ SNoL x0}, λ x1 x2 . x2 = SNoL x0.

Apply set_ext with {add_SNo 0 x1|x1 ∈ SNoL x0}, SNoL x0 leaving 2 subgoals.

Let x1 of type ι be given.

Assume H2: x1 ∈ {add_SNo 0 x2|x2 ∈ SNoL x0}.

Apply ReplE_impred with SNoL x0, λ x2 . add_SNo 0 ..., ..., ... leaving 2 subgoals.

...

Claim L3: binunion {add_SNo x1 x0|x1 ∈ SNoR 0} {add_SNo 0 x1|x1 ∈ SNoR x0} = SNoR x0

Apply SNoR_0 with λ x1 x2 . binunion {add_SNo x3 x0|x3 ∈ x2} {add_SNo 0 x3|x3 ∈ SNoR x0} = SNoR x0.

Apply Repl_Empty with λ x1 . add_SNo x1 x0, λ x1 x2 . binunion x2 {add_SNo 0 x3|x3 ∈ SNoR x0} = SNoR x0.

Apply binunion_idl with {add_SNo 0 x1|x1 ∈ SNoR x0}, λ x1 x2 . x2 = SNoR x0.

Apply set_ext with {add_SNo 0 x1|x1 ∈ SNoR x0}, SNoR x0 leaving 2 subgoals.

Let x1 of type ι be given.

Assume H3: x1 ∈ {add_SNo 0 x2|x2 ∈ SNoR x0}.

Apply ReplE_impred with SNoR x0, λ x2 . add_SNo 0 x2, x1, x1 ∈ SNoR x0 leaving 2 subgoals.

The subproof is completed by applying H3.

Let x2 of type ι be given.

Assume H4: x2 ∈ SNoR x0.

Assume H5: x1 = add_SNo 0 x2.

Apply H5 with λ x3 x4 . x4 ∈ SNoR x0.

Apply H1 with x2, λ x3 x4 . x4 ∈ SNoR x0 leaving 2 subgoals.

Apply SNoR_SNoS_ with x0, x2.

The subproof is completed by applying H4.

Let x1 of type ι be given.

Assume H3: x1 ∈ SNoR x0.

Apply H1 with x1, λ x2 x3 . x2 ∈ {add_SNo 0 x4|x4 ∈ SNoR x0} leaving 2 subgoals.

Apply SNoR_SNoS_ with x0, x1.

The subproof is completed by applying H3.

Apply ReplI with SNoR x0, λ x2 . add_SNo 0 x2, x1.

The subproof is completed by applying H3.

Apply L2 with λ x1 x2 . SNoCut x2 (binunion {add_SNo x3 x0|x3 ∈ SNoR 0} {add_SNo 0 x3|x3 ∈ SNoR x0}) = x0.

Apply L3 with λ x1 x2 . SNoCut (SNoL x0) x2 = x0.

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

Apply SNo_eta with x0, λ x2 x3 . x1 x3 x2.

The subproof is completed by applying H0.

■

Proofgold Proof