Set P to be the term λx y ⇒ SNoLev (x + y) ⊆ SNoLev x + SNoLev y of type set → set → prop.
Apply SNoLev_ind2 to the current goal.
Let x and y be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
We prove the intermediate claim Lxy: SNo (x + y).
An exact proof term for the current goal is SNo_add_SNo x y Hx Hy.
We prove the intermediate claim LLxLy: ordinal (SNoLev x + SNoLev y).
Apply add_SNo_ordinal_ordinal to the current goal.
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is Hx.
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is Hy.
Assume IH1: ∀w ∈ SNoS_ (SNoLev x), P w y.
Assume IH2: ∀z ∈ SNoS_ (SNoLev y), P x z.
Assume IH3: ∀w ∈ SNoS_ (SNoLev x), ∀z ∈ SNoS_ (SNoLev y), P w z.
We will prove SNoLev (x + y) ⊆ SNoLev x + SNoLev y.
Set Lxy1 to be the term {w + y|w ∈ SNoL x}.
Set Lxy2 to be the term {x + w|w ∈ SNoL y}.
Set Rxy1 to be the term {z + y|z ∈ SNoR x}.
Set Rxy2 to be the term {x + z|z ∈ SNoR y}.
rewrite the current goal using add_SNo_eq x Hx y Hy (from left to right).
We will prove SNoLev (SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2)) ⊆ SNoLev x + SNoLev y.
We prove the intermediate claim L1: SNoCutP (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2).
An exact proof term for the current goal is add_SNo_SNoCutP x y Hx Hy.
Apply SNoCutP_SNoCut_impred (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2) L1 to the current goal.
Assume H1: SNo (SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2)).
Assume H2: SNoLev (SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2)) ∈ ordsucc ((⋃x ∈ (Lxy1 ∪ Lxy2)ordsucc (SNoLev x)) ∪ (⋃y ∈ (Rxy1 ∪ Rxy2)ordsucc (SNoLev y))).
Assume _ _ _.
We prove the intermediate claim Lxy1E: ∀u ∈ Lxy1, ∀p : set → prop, (∀w ∈ SNoS_ (SNoLev x), u = w + y → SNo w → SNoLev w ∈ SNoLev x → w < x → p (w + y)) → p u.
Let u be given.
Assume Hu.
Let p be given.
Assume Hp.
Apply ReplE_impred (SNoL x) (λw ⇒ w + y) u Hu to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL x.
Assume Huw: u = w + y.
rewrite the current goal using Huw (from left to right).
Apply SNoL_E x Hx w Hw to the current goal.
We prove the intermediate claim Lw: w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoL_SNoS_ x w Hw.
An exact proof term for the current goal is Hp w Lw Huw.
We prove the intermediate claim Lxy2E: ∀u ∈ Lxy2, ∀p : set → prop, (∀w ∈ SNoS_ (SNoLev y), u = x + w → SNo w → SNoLev w ∈ SNoLev y → w < y → p (x + w)) → p u.
Let u be given.
Assume Hu.
Let p be given.
Assume Hp.
Apply ReplE_impred (SNoL y) (λw ⇒ x + w) u Hu to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL y.
Assume Huw: u = x + w.
rewrite the current goal using Huw (from left to right).
Apply SNoL_E y Hy w Hw to the current goal.
We prove the intermediate claim Lw: w ∈ SNoS_ (SNoLev y).
An exact proof term for the current goal is SNoL_SNoS_ y w Hw.
An exact proof term for the current goal is Hp w Lw Huw.
We prove the intermediate claim Rxy1E: ∀u ∈ Rxy1, ∀p : set → prop, (∀w ∈ SNoS_ (SNoLev x), u = w + y → SNo w → SNoLev w ∈ SNoLev x → x < w → p (w + y)) → p u.
Let u be given.
Assume Hu.
Let p be given.
Assume Hp.
Apply ReplE_impred (SNoR x) (λw ⇒ w + y) u Hu to the current goal.
Let w be given.
Assume Hw: w ∈ SNoR x.
Assume Huw: u = w + y.
rewrite the current goal using Huw (from left to right).
Apply SNoR_E x Hx w Hw to the current goal.
We prove the intermediate claim Lw: w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoR_SNoS_ x w Hw.
An exact proof term for the current goal is Hp w Lw Huw.
We prove the intermediate claim Rxy2E: ∀u ∈ Rxy2, ∀p : set → prop, (∀w ∈ SNoS_ (SNoLev y), u = x + w → SNo w → SNoLev w ∈ SNoLev y → y < w → p (x + w)) → p u.
Let u be given.
Assume Hu.
Let p be given.
Assume Hp.
Apply ReplE_impred (SNoR y) (λw ⇒ x + w) u Hu to the current goal.
Let w be given.
Assume Hw: w ∈ SNoR y.
Assume Huw: u = x + w.
rewrite the current goal using Huw (from left to right).
Apply SNoR_E y Hy w Hw to the current goal.
We prove the intermediate claim Lw: w ∈ SNoS_ (SNoLev y).
An exact proof term for the current goal is SNoR_SNoS_ y w Hw.
An exact proof term for the current goal is Hp w Lw Huw.
We prove the intermediate claim Lxy1E2: ∀u ∈ Lxy1, SNo u.
Let u be given.
Assume Hu.
Apply Lxy1E u Hu to the current goal.
Let w be given.
Assume Hw1 Hw2 Hw3 Hw4 Hw5.
We will prove SNo (w + y).
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hw3.
An exact proof term for the current goal is Hy.
We prove the intermediate claim Lxy2E2: ∀u ∈ Lxy2, SNo u.
Let u be given.
Assume Hu.
Apply Lxy2E u Hu to the current goal.
Let w be given.
Assume Hw1 Hw2 Hw3 Hw4 Hw5.
We will prove SNo (x + w).
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hw3.
We prove the intermediate claim Rxy1E2: ∀u ∈ Rxy1, SNo u.
Let u be given.
Assume Hu.
Apply Rxy1E u Hu to the current goal.
Let w be given.
Assume Hw1 Hw2 Hw3 Hw4 Hw5.
We will prove SNo (w + y).
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hw3.
An exact proof term for the current goal is Hy.
We prove the intermediate claim Rxy2E2: ∀u ∈ Rxy2, SNo u.
Let u be given.
Assume Hu.
Apply Rxy2E u Hu to the current goal.
Let w be given.
Assume Hw1 Hw2 Hw3 Hw4 Hw5.
We will prove SNo (x + w).
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hw3.
We prove the intermediate claim L2: ordinal ((⋃u ∈ (Lxy1 ∪ Lxy2)ordsucc (SNoLev u)) ∪ (⋃u ∈ (Rxy1 ∪ Rxy2)ordsucc (SNoLev u))).
Apply ordinal_binunion to the current goal.
Apply ordinal_famunion (Lxy1 ∪ Lxy2) (λu ⇒ ordsucc (SNoLev u)) to the current goal.
Let u be given.
Assume Hu: u ∈ Lxy1 ∪ Lxy2.
We will prove ordinal (ordsucc (SNoLev u)).
Apply ordinal_ordsucc to the current goal.
Apply SNoLev_ordinal to the current goal.
We will prove SNo u.
Apply binunionE Lxy1 Lxy2 u Hu to the current goal.
Assume Hu.
An exact proof term for the current goal is Lxy1E2 u Hu.
Assume Hu.
An exact proof term for the current goal is Lxy2E2 u Hu.
Apply ordinal_famunion (Rxy1 ∪ Rxy2) (λu ⇒ ordsucc (SNoLev u)) to the current goal.
Let u be given.
Assume Hu: u ∈ Rxy1 ∪ Rxy2.
We will prove ordinal (ordsucc (SNoLev u)).
Apply ordinal_ordsucc to the current goal.
Apply SNoLev_ordinal to the current goal.
We will prove SNo u.
Apply binunionE Rxy1 Rxy2 u Hu to the current goal.
Assume Hu.
An exact proof term for the current goal is Rxy1E2 u Hu.
Assume Hu.
An exact proof term for the current goal is Rxy2E2 u Hu.
We prove the intermediate claim L3: SNoLev (SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2)) ⊆ (⋃u ∈ (Lxy1 ∪ Lxy2)ordsucc (SNoLev u)) ∪ (⋃u ∈ (Rxy1 ∪ Rxy2)ordsucc (SNoLev u)).
Apply TransSet_In_ordsucc_Subq to the current goal.
We will prove TransSet ((⋃u ∈ (Lxy1 ∪ Lxy2)ordsucc (SNoLev u)) ∪ (⋃u ∈ (Rxy1 ∪ Rxy2)ordsucc (SNoLev u))).
Apply L2 to the current goal.
Assume H _.
An exact proof term for the current goal is H.
An exact proof term for the current goal is H2.
We prove the intermediate claim L4: ((⋃u ∈ (Lxy1 ∪ Lxy2)ordsucc (SNoLev u)) ∪ (⋃u ∈ (Rxy1 ∪ Rxy2)ordsucc (SNoLev u))) ⊆ SNoLev x + SNoLev y.
Apply binunion_Subq_min to the current goal.
We will prove (⋃u ∈ (Lxy1 ∪ Lxy2)ordsucc (SNoLev u)) ⊆ SNoLev x + SNoLev y.
Let v be given.
Assume Hv: v ∈ (⋃u ∈ (Lxy1 ∪ Lxy2)ordsucc (SNoLev u)).
Apply famunionE_impred (Lxy1 ∪ Lxy2) (λu ⇒ ordsucc (SNoLev u)) v Hv to the current goal.
Let u be given.
Assume Hu: u ∈ Lxy1 ∪ Lxy2.
Apply binunionE Lxy1 Lxy2 u Hu to the current goal.
Assume Hu: u ∈ Lxy1.
Apply Lxy1E u Hu to the current goal.
Let w be given.
Assume Hw1: w ∈ SNoS_ (SNoLev x).
Assume Hw2: u = w + y.
Assume Hw3: SNo w.
Assume Hw4: SNoLev w ∈ SNoLev x.
Assume Hw5: w < x.
Assume Hw6: v ∈ ordsucc (SNoLev (w + y)).
We will prove v ∈ SNoLev x + SNoLev y.
We prove the intermediate claim Lv: ordinal v.
Apply ordinal_Hered (ordsucc (SNoLev (w + y))) to the current goal.
We will prove ordinal (ordsucc (SNoLev (w + y))).
Apply ordinal_ordsucc to the current goal.
Apply SNoLev_ordinal to the current goal.
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hw3.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is Hw6.
Apply ordinal_In_Or_Subq v (SNoLev x + SNoLev y) Lv LLxLy to the current goal.
Assume H1: v ∈ SNoLev x + SNoLev y.
An exact proof term for the current goal is H1.
Assume H1: SNoLev x + SNoLev y ⊆ v.
We will prove False.
We prove the intermediate claim LIHw: SNoLev (w + y) ⊆ SNoLev w + SNoLev y.
Apply IH1 to the current goal.
We will prove w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is Hw1.
We prove the intermediate claim L4a: SNoLev w + SNoLev y ∈ SNoLev x + SNoLev y.
Apply add_SNo_ordinal_InL to the current goal.
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is Hx.
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is Hw4.
We prove the intermediate claim L4b: SNoLev w + SNoLev y ⊆ SNoLev x + SNoLev y.
Apply LLxLy to the current goal.
Assume H _.
An exact proof term for the current goal is H (SNoLev w + SNoLev y) L4a.
We prove the intermediate claim L4c: v ⊆ SNoLev (w + y).
Apply ordinal_In_Or_Subq (SNoLev (w + y)) v (SNoLev_ordinal (w + y) (SNo_add_SNo w y Hw3 Hy)) Lv to the current goal.
Assume H2: SNoLev (w + y) ∈ v.
We will prove False.
Apply ordsuccE (SNoLev (w + y)) v Hw6 to the current goal.
Assume H3: v ∈ SNoLev (w + y).
An exact proof term for the current goal is In_no2cycle (SNoLev (w + y)) v H2 H3.
Assume H3: v = SNoLev (w + y).
Apply In_irref v to the current goal.
rewrite the current goal using H3 (from left to right) at position 1.
An exact proof term for the current goal is H2.
Assume H2: v ⊆ SNoLev (w + y).
An exact proof term for the current goal is H2.
Apply In_irref (SNoLev w + SNoLev y) to the current goal.
We will prove (SNoLev w + SNoLev y) ∈ (SNoLev w + SNoLev y).
Apply LIHw to the current goal.
We will prove (SNoLev w + SNoLev y) ∈ SNoLev (w + y).
Apply L4c to the current goal.
We will prove (SNoLev w + SNoLev y) ∈ v.
Apply H1 to the current goal.
We will prove (SNoLev w + SNoLev y) ∈ SNoLev x + SNoLev y.
An exact proof term for the current goal is L4a.
Assume Hu: u ∈ Lxy2.
Apply Lxy2E u Hu to the current goal.
Let w be given.
Assume Hw1: w ∈ SNoS_ (SNoLev y).
Assume Hw2: u = x + w.
Assume Hw3: SNo w.
Assume Hw4: SNoLev w ∈ SNoLev y.
Assume Hw5: w < y.
Assume Hw6: v ∈ ordsucc (SNoLev (x + w)).
We will prove v ∈ SNoLev x + SNoLev y.
We prove the intermediate claim Lv: ordinal v.
Apply ordinal_Hered (ordsucc (SNoLev (x + w))) to the current goal.
We will prove ordinal (ordsucc (SNoLev (x + w))).
Apply ordinal_ordsucc to the current goal.
Apply SNoLev_ordinal to the current goal.
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hw3.
An exact proof term for the current goal is Hw6.
Apply ordinal_In_Or_Subq v (SNoLev x + SNoLev y) Lv LLxLy to the current goal.
Assume H1: v ∈ SNoLev x + SNoLev y.
An exact proof term for the current goal is H1.
Assume H1: SNoLev x + SNoLev y ⊆ v.
We will prove False.
We prove the intermediate claim LIHw: SNoLev (x + w) ⊆ SNoLev x + SNoLev w.
Apply IH2 to the current goal.
We will prove w ∈ SNoS_ (SNoLev y).
An exact proof term for the current goal is Hw1.
We prove the intermediate claim L4a: SNoLev x + SNoLev w ∈ SNoLev x + SNoLev y.
Apply add_SNo_ordinal_InR to the current goal.
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is Hx.
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is Hw4.
We prove the intermediate claim L4b: SNoLev x + SNoLev w ⊆ SNoLev x + SNoLev y.
Apply LLxLy to the current goal.
Assume H _.
An exact proof term for the current goal is H (SNoLev x + SNoLev w) L4a.
We prove the intermediate claim L4c: v ⊆ SNoLev (x + w).
Apply ordinal_In_Or_Subq (SNoLev (x + w)) v (SNoLev_ordinal (x + w) (SNo_add_SNo x w Hx Hw3)) Lv to the current goal.
Assume H2: SNoLev (x + w) ∈ v.
We will prove False.
Apply ordsuccE (SNoLev (x + w)) v Hw6 to the current goal.
Assume H3: v ∈ SNoLev (x + w).
An exact proof term for the current goal is In_no2cycle (SNoLev (x + w)) v H2 H3.
Assume H3: v = SNoLev (x + w).
Apply In_irref v to the current goal.
rewrite the current goal using H3 (from left to right) at position 1.
An exact proof term for the current goal is H2.
Assume H2: v ⊆ SNoLev (x + w).
An exact proof term for the current goal is H2.
Apply In_irref (SNoLev x + SNoLev w) to the current goal.
We will prove (SNoLev x + SNoLev w) ∈ (SNoLev x + SNoLev w).
Apply LIHw to the current goal.
We will prove (SNoLev x + SNoLev w) ∈ SNoLev (x + w).
Apply L4c to the current goal.
We will prove (SNoLev x + SNoLev w) ∈ v.
Apply H1 to the current goal.
We will prove (SNoLev x + SNoLev w) ∈ SNoLev x + SNoLev y.
An exact proof term for the current goal is L4a.
We will prove (⋃u ∈ (Rxy1 ∪ Rxy2)ordsucc (SNoLev u)) ⊆ SNoLev x + SNoLev y.
Let v be given.
Assume Hv: v ∈ (⋃u ∈ (Rxy1 ∪ Rxy2)ordsucc (SNoLev u)).
Apply famunionE_impred (Rxy1 ∪ Rxy2) (λu ⇒ ordsucc (SNoLev u)) v Hv to the current goal.
Let u be given.
Assume Hu: u ∈ Rxy1 ∪ Rxy2.
Apply binunionE Rxy1 Rxy2 u Hu to the current goal.
Assume Hu: u ∈ Rxy1.
Apply Rxy1E u Hu to the current goal.
Let w be given.
Assume Hw1: w ∈ SNoS_ (SNoLev x).
Assume Hw2: u = w + y.
Assume Hw3: SNo w.
Assume Hw4: SNoLev w ∈ SNoLev x.
Assume Hw5: x < w.
Assume Hw6: v ∈ ordsucc (SNoLev (w + y)).
We will prove v ∈ SNoLev x + SNoLev y.
We prove the intermediate claim Lv: ordinal v.
Apply ordinal_Hered (ordsucc (SNoLev (w + y))) to the current goal.
We will prove ordinal (ordsucc (SNoLev (w + y))).
Apply ordinal_ordsucc to the current goal.
Apply SNoLev_ordinal to the current goal.
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hw3.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is Hw6.
Apply ordinal_In_Or_Subq v (SNoLev x + SNoLev y) Lv LLxLy to the current goal.
Assume H1: v ∈ SNoLev x + SNoLev y.
An exact proof term for the current goal is H1.
Assume H1: SNoLev x + SNoLev y ⊆ v.
We will prove False.
We prove the intermediate claim LIHw: SNoLev (w + y) ⊆ SNoLev w + SNoLev y.
Apply IH1 to the current goal.
We will prove w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is Hw1.
We prove the intermediate claim L4a: SNoLev w + SNoLev y ∈ SNoLev x + SNoLev y.
Apply add_SNo_ordinal_InL to the current goal.
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is Hx.
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is Hw4.
We prove the intermediate claim L4b: SNoLev w + SNoLev y ⊆ SNoLev x + SNoLev y.
Apply LLxLy to the current goal.
Assume H _.
An exact proof term for the current goal is H (SNoLev w + SNoLev y) L4a.
We prove the intermediate claim L4c: v ⊆ SNoLev (w + y).
Apply ordinal_In_Or_Subq (SNoLev (w + y)) v (SNoLev_ordinal (w + y) (SNo_add_SNo w y Hw3 Hy)) Lv to the current goal.
Assume H2: SNoLev (w + y) ∈ v.
We will prove False.
Apply ordsuccE (SNoLev (w + y)) v Hw6 to the current goal.
Assume H3: v ∈ SNoLev (w + y).
An exact proof term for the current goal is In_no2cycle (SNoLev (w + y)) v H2 H3.
Assume H3: v = SNoLev (w + y).
Apply In_irref v to the current goal.
rewrite the current goal using H3 (from left to right) at position 1.
An exact proof term for the current goal is H2.
Assume H2: v ⊆ SNoLev (w + y).
An exact proof term for the current goal is H2.
Apply In_irref (SNoLev w + SNoLev y) to the current goal.
We will prove (SNoLev w + SNoLev y) ∈ (SNoLev w + SNoLev y).
Apply LIHw to the current goal.
We will prove (SNoLev w + SNoLev y) ∈ SNoLev (w + y).
Apply L4c to the current goal.
We will prove (SNoLev w + SNoLev y) ∈ v.
Apply H1 to the current goal.
We will prove (SNoLev w + SNoLev y) ∈ SNoLev x + SNoLev y.
An exact proof term for the current goal is L4a.
Assume Hu: u ∈ Rxy2.
Apply Rxy2E u Hu to the current goal.
Let w be given.
Assume Hw1: w ∈ SNoS_ (SNoLev y).
Assume Hw2: u = x + w.
Assume Hw3: SNo w.
Assume Hw4: SNoLev w ∈ SNoLev y.
Assume Hw5: y < w.
Assume Hw6: v ∈ ordsucc (SNoLev (x + w)).
We will prove v ∈ SNoLev x + SNoLev y.
We prove the intermediate claim Lv: ordinal v.
Apply ordinal_Hered (ordsucc (SNoLev (x + w))) to the current goal.
We will prove ordinal (ordsucc (SNoLev (x + w))).
Apply ordinal_ordsucc to the current goal.
Apply SNoLev_ordinal to the current goal.
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hw3.
An exact proof term for the current goal is Hw6.
Apply ordinal_In_Or_Subq v (SNoLev x + SNoLev y) Lv LLxLy to the current goal.
Assume H1: v ∈ SNoLev x + SNoLev y.
An exact proof term for the current goal is H1.
Assume H1: SNoLev x + SNoLev y ⊆ v.
We will prove False.
We prove the intermediate claim LIHw: SNoLev (x + w) ⊆ SNoLev x + SNoLev w.
Apply IH2 to the current goal.
We will prove w ∈ SNoS_ (SNoLev y).
An exact proof term for the current goal is Hw1.
We prove the intermediate claim L4a: SNoLev x + SNoLev w ∈ SNoLev x + SNoLev y.
Apply add_SNo_ordinal_InR to the current goal.
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is Hx.
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is Hw4.
We prove the intermediate claim L4b: SNoLev x + SNoLev w ⊆ SNoLev x + SNoLev y.
Apply LLxLy to the current goal.
Assume H _.
An exact proof term for the current goal is H (SNoLev x + SNoLev w) L4a.
We prove the intermediate claim L4c: v ⊆ SNoLev (x + w).
Apply ordinal_In_Or_Subq (SNoLev (x + w)) v (SNoLev_ordinal (x + w) (SNo_add_SNo x w Hx Hw3)) Lv to the current goal.
Assume H2: SNoLev (x + w) ∈ v.
We will prove False.
Apply ordsuccE (SNoLev (x + w)) v Hw6 to the current goal.
Assume H3: v ∈ SNoLev (x + w).
An exact proof term for the current goal is In_no2cycle (SNoLev (x + w)) v H2 H3.
Assume H3: v = SNoLev (x + w).
Apply In_irref v to the current goal.
rewrite the current goal using H3 (from left to right) at position 1.
An exact proof term for the current goal is H2.
Assume H2: v ⊆ SNoLev (x + w).
An exact proof term for the current goal is H2.
Apply In_irref (SNoLev x + SNoLev w) to the current goal.
We will prove (SNoLev x + SNoLev w) ∈ (SNoLev x + SNoLev w).
Apply LIHw to the current goal.
We will prove (SNoLev x + SNoLev w) ∈ SNoLev (x + w).
Apply L4c to the current goal.
We will prove (SNoLev x + SNoLev w) ∈ v.
Apply H1 to the current goal.
We will prove (SNoLev x + SNoLev w) ∈ SNoLev x + SNoLev y.
An exact proof term for the current goal is L4a.
An exact proof term for the current goal is Subq_tra (SNoLev (SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2))) ((⋃u ∈ (Lxy1 ∪ Lxy2)ordsucc (SNoLev u)) ∪ (⋃u ∈ (Rxy1 ∪ Rxy2)ordsucc (SNoLev u))) (SNoLev x + SNoLev y) L3 L4.
∎