Let x be given.
Assume Hx.
We prove the intermediate claim L1: SNo (SNo_extend1 x).
An exact proof term for the current goal is SNo_extend1_SNo x Hx.
We prove the intermediate claim L2: SNoLev x ∈ SNoLev (SNo_extend1 x).
rewrite the current goal using SNo_extend1_SNoLev x Hx (from left to right).
Apply ordsuccI2 to the current goal.
Apply SNo_eq to the current goal.
An exact proof term for the current goal is Hx.
Apply restr_SNo to the current goal.
An exact proof term for the current goal is L1.
An exact proof term for the current goal is L2.
We will prove SNoLev x = SNoLev (SNo_extend1 x ∩ SNoElts_ (SNoLev x)).
Use symmetry.
Apply restr_SNoLev to the current goal.
An exact proof term for the current goal is L1.
An exact proof term for the current goal is L2.
We will prove SNoEq_ (SNoLev x) x (SNo_extend1 x ∩ SNoElts_ (SNoLev x)).
Apply SNoEq_sym_ to the current goal.
Apply SNoEq_tra_ (SNoLev x) (SNo_extend1 x ∩ SNoElts_ (SNoLev x)) (SNo_extend1 x) x to the current goal.
We will prove SNoEq_ (SNoLev x) (SNo_extend1 x ∩ SNoElts_ (SNoLev x)) (SNo_extend1 x).
An exact proof term for the current goal is restr_SNoEq (SNo_extend1 x) L1 (SNoLev x) L2.
We will prove SNoEq_ (SNoLev x) (SNo_extend1 x) x.
An exact proof term for the current goal is SNo_extend1_SNoEq x Hx.
∎