Apply SNoCutP_SNoCut_impred 0 0 SNoCutP_0_0 to the current goal.
Assume H1: SNo (SNoCut 0 0).
rewrite the current goal using famunion_Empty (λx ⇒ ordsucc (SNoLev x)) (from left to right).
rewrite the current goal using binunion_idl 0 (from left to right).
Assume H2: SNoLev (SNoCut 0 0) ∈ 1.
Assume _ _ _.
We prove the intermediate claim L1: SNoLev (SNoCut 0 0) = 0.
Apply cases_1 (SNoLev (SNoCut 0 0)) H2 (λu ⇒ u = 0) to the current goal.
We will prove 0 = 0.
Use reflexivity.
Apply SNo_eq (SNoCut 0 0) 0 H1 SNo_0 to the current goal.
We will prove SNoLev (SNoCut 0 0) = SNoLev 0.
Use transitivity with and 0.
An exact proof term for the current goal is L1.
Use symmetry.
An exact proof term for the current goal is SNoLev_0.
We will prove SNoEq_ (SNoLev (SNoCut 0 0)) (SNoCut 0 0) 0.
rewrite the current goal using L1 (from left to right).
We will prove SNoEq_ 0 (SNoCut 0 0) 0.
Apply SNoEq_I to the current goal.
Let β be given.
Assume Hb: β ∈ 0.
We will prove False.
An exact proof term for the current goal is EmptyE β Hb.
∎