Let L and R be given.
Assume HC: SNoCutP L R.
Apply HC to the current goal.
Assume HC.
Apply HC to the current goal.
Assume HL: ∀x ∈ L, SNo x.
Assume HR: ∀y ∈ R, SNo y.
Assume HLR: ∀x ∈ L, ∀y ∈ R, x < y.
Set L' to be the term λα p ⇒ ordinal α ∧ PSNo α p ∈ L of type set → (set → prop) → prop.
Set R' to be the term λα p ⇒ ordinal α ∧ PSNo α p ∈ R of type set → (set → prop) → prop.
Set tau to be the term PNo_bd L' R'.
Set w to be the term PNo_pred L' R'.
Set alpha to be the term ⋃x ∈ Lordsucc (SNoLev x).
Set beta to be the term ⋃y ∈ Rordsucc (SNoLev y).
We will prove SNo (SNoCut L R) ∧ SNoLev (SNoCut L R) ∈ ordsucc (α ∪ β) ∧ (∀x ∈ L, x < SNoCut L R) ∧ (∀y ∈ R, SNoCut L R < y) ∧ (∀z, SNo z → (∀x ∈ L, x < z) → (∀y ∈ R, z < y) → SNoLev (SNoCut L R) ⊆ SNoLev z ∧ PNoEq_ (SNoLev (SNoCut L R)) (λγ ⇒ γ ∈ SNoCut L R) (λγ ⇒ γ ∈ z)).
We prove the intermediate claim LLR: PNoLt_pwise L' R'.
Let γ be given.
Assume Hc: ordinal γ.
Let p be given.
Assume H1: L' γ p.
Apply H1 to the current goal.
Assume _ H1.
Let δ be given.
Assume Hd: ordinal δ.
Let q be given.
Assume H2: R' δ q.
Apply H2 to the current goal.
Assume _ H2.
We will prove PNoLt γ p δ q.
Apply SNoLt_PSNo_PNoLt γ δ p q Hc Hd to the current goal.
We will prove PSNo γ p < PSNo δ q.
An exact proof term for the current goal is HLR (PSNo γ p) H1 (PSNo δ q) H2.
We prove the intermediate claim La: ordinal α.
Apply ordinal_famunion L (λx ⇒ ordsucc (SNoLev x)) to the current goal.
Let x be given.
Assume Hx: x ∈ L.
We will prove ordinal (ordsucc (SNoLev x)).
Apply ordinal_ordsucc to the current goal.
Apply SNoLev_ordinal to the current goal.
We will prove SNo x.
An exact proof term for the current goal is HL x Hx.
We prove the intermediate claim Lb: ordinal β.
Apply ordinal_famunion R (λy ⇒ ordsucc (SNoLev y)) to the current goal.
Let y be given.
Assume Hy: y ∈ R.
We will prove ordinal (ordsucc (SNoLev y)).
Apply ordinal_ordsucc to the current goal.
Apply SNoLev_ordinal to the current goal.
We will prove SNo y.
An exact proof term for the current goal is HR y Hy.
We prove the intermediate claim Lab: ordinal (α ∪ β).
Apply ordinal_linear α β La Lb to the current goal.
We will prove α ⊆ β → ordinal (α ∪ β).
rewrite the current goal using Subq_binunion_eq α β (from left to right).
We will prove α ∪ β = β → ordinal (α ∪ β).
Assume H1.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Lb.
We will prove β ⊆ α → ordinal (α ∪ β).
rewrite the current goal using Subq_binunion_eq β α (from left to right).
We will prove β ∪ α = α → ordinal (α ∪ β).
Assume H1.
rewrite the current goal using binunion_com (from left to right).
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is La.
We prove the intermediate claim LLab: PNo_lenbdd (α ∪ β) L'.
Let γ be given.
Let p be given.
Assume H1.
Apply H1 to the current goal.
Assume H1: ordinal γ.
Assume H2: PSNo γ p ∈ L.
We will prove γ ∈ α ∪ β.
Apply binunionI1 to the current goal.
We will prove γ ∈ ⋃x ∈ Lordsucc (SNoLev x).
Apply famunionI L (λx ⇒ ordsucc (SNoLev x)) (PSNo γ p) γ to the current goal.
We will prove PSNo γ p ∈ L.
An exact proof term for the current goal is H2.
We will prove γ ∈ ordsucc (SNoLev (PSNo γ p)).
rewrite the current goal using SNoLev_PSNo γ H1 p (from left to right).
We will prove γ ∈ ordsucc γ.
Apply ordsuccI2 to the current goal.
We prove the intermediate claim LRab: PNo_lenbdd (α ∪ β) R'.
Let γ be given.
Let p be given.
Assume H1.
Apply H1 to the current goal.
Assume H1: ordinal γ.
Assume H2: PSNo γ p ∈ R.
We will prove γ ∈ α ∪ β.
Apply binunionI2 to the current goal.
We will prove γ ∈ ⋃y ∈ Rordsucc (SNoLev y).
Apply famunionI R (λy ⇒ ordsucc (SNoLev y)) (PSNo γ p) γ to the current goal.
We will prove PSNo γ p ∈ R.
An exact proof term for the current goal is H2.
We will prove γ ∈ ordsucc (SNoLev (PSNo γ p)).
rewrite the current goal using SNoLev_PSNo γ H1 p (from left to right).
We will prove γ ∈ ordsucc γ.
Apply ordsuccI2 to the current goal.
Apply PNo_bd_pred L' R' LLR (α ∪ β) Lab LLab LRab to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: ordinal tau.
Assume H2: PNo_strict_imv L' R' tau w.
Assume H3: ∀γ ∈ tau, ∀q : set → prop, ¬ PNo_strict_imv L' R' γ q.
Apply H2 to the current goal.
Assume H4: PNo_strict_upperbd L' tau w.
Assume H5: PNo_strict_lowerbd R' tau w.
We prove the intermediate claim LNoC: SNo (SNoCut L R).
We will prove SNo (PSNo tau w).
We will prove ∃α, ordinal α ∧ SNo_ α (PSNo tau w).
We use tau to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H1.
We will prove SNo_ tau (PSNo tau w).
Apply SNo_PSNo tau to the current goal.
We will prove ordinal tau.
An exact proof term for the current goal is H1.
We prove the intermediate claim LLleveqtau: SNoLev (SNoCut L R) = tau.
An exact proof term for the current goal is SNoLev_PSNo tau H1 (PNo_pred L' R').
We prove the intermediate claim LLbdtau: tau ∈ ordsucc (α ∪ β).
An exact proof term for the current goal is PNo_bd_In L' R' LLR (α ∪ β) Lab LLab LRab.
We prove the intermediate claim LLbd: SNoLev (SNoCut L R) ∈ ordsucc (α ∪ β).
rewrite the current goal using LLleveqtau (from left to right).
An exact proof term for the current goal is LLbdtau.
We prove the intermediate claim LLecw: PNoEq_ tau (λγ ⇒ γ ∈ SNoCut L R) w.
We will prove PNoEq_ tau (λγ ⇒ γ ∈ PSNo tau w) w.
An exact proof term for the current goal is PNoEq_PSNo tau H1 w.
We prove the intermediate claim LLC: ordinal (SNoLev (SNoCut L R)).
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is LNoC.
We prove the intermediate claim LL: ∀x ∈ L, x < SNoCut L R.
Let x be given.
Assume Hx: x ∈ L.
We will prove x < SNoCut L R.
We will prove x < PSNo tau w.
We prove the intermediate claim L1: SNo x.
An exact proof term for the current goal is HL x Hx.
We prove the intermediate claim LLx: ordinal (SNoLev x).
An exact proof term for the current goal is SNoLev_ordinal x L1.
We prove the intermediate claim L2: x = PSNo (SNoLev x) (λγ ⇒ γ ∈ x).
Apply SNo_PSNo_eta to the current goal.
An exact proof term for the current goal is L1.
We prove the intermediate claim L3: L' (SNoLev x) (λγ ⇒ γ ∈ x).
We will prove ordinal (SNoLev x) ∧ PSNo (SNoLev x) (λγ ⇒ γ ∈ x) ∈ L.
Apply andI to the current goal.
An exact proof term for the current goal is LLx.
rewrite the current goal using L2 (from right to left).
An exact proof term for the current goal is Hx.
We will prove x < PSNo tau w.
rewrite the current goal using L2 (from left to right).
Apply PNoLt_SNoLt_PSNo (SNoLev x) tau (λγ ⇒ γ ∈ x) w LLx H1 to the current goal.
We will prove PNoLt (SNoLev x) (λγ ⇒ γ ∈ x) tau w.
An exact proof term for the current goal is H4 (SNoLev x) LLx (λγ ⇒ γ ∈ x) L3.
We prove the intermediate claim LR: ∀y ∈ R, SNoCut L R < y.
Let y be given.
Assume Hy: y ∈ R.
We will prove SNoCut L R < y.
We will prove PSNo tau w < y.
We prove the intermediate claim L1: SNo y.
An exact proof term for the current goal is HR y Hy.
We prove the intermediate claim LLy: ordinal (SNoLev y).
An exact proof term for the current goal is SNoLev_ordinal y L1.
We prove the intermediate claim L2: y = PSNo (SNoLev y) (λγ ⇒ γ ∈ y).
Apply SNo_PSNo_eta to the current goal.
An exact proof term for the current goal is L1.
We prove the intermediate claim L3: R' (SNoLev y) (λγ ⇒ γ ∈ y).
We will prove ordinal (SNoLev y) ∧ PSNo (SNoLev y) (λγ ⇒ γ ∈ y) ∈ R.
Apply andI to the current goal.
An exact proof term for the current goal is LLy.
rewrite the current goal using L2 (from right to left).
An exact proof term for the current goal is Hy.
We will prove PSNo tau w < y.
rewrite the current goal using L2 (from left to right).
Apply PNoLt_SNoLt_PSNo tau (SNoLev y) w (λγ ⇒ γ ∈ y) H1 LLy to the current goal.
We will prove PNoLt tau w (SNoLev y) (λγ ⇒ γ ∈ y).
An exact proof term for the current goal is H5 (SNoLev y) LLy (λγ ⇒ γ ∈ y) L3.
Apply and5I to the current goal.
An exact proof term for the current goal is LNoC.
An exact proof term for the current goal is LLbd.
An exact proof term for the current goal is LL.
An exact proof term for the current goal is LR.
We will prove ∀z, SNo z → (∀x ∈ L, x < z) → (∀y ∈ R, z < y) → SNoLev (SNoCut L R) ⊆ SNoLev z ∧ PNoEq_ (SNoLev (SNoCut L R)) (λγ ⇒ γ ∈ SNoCut L R) (λγ ⇒ γ ∈ z).
Let z be given.
Assume Hz: SNo z.
Assume H10: ∀x ∈ L, x < z.
Assume H11: ∀y ∈ R, z < y.
We prove the intermediate claim LLz: ordinal (SNoLev z).
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is Hz.
We prove the intermediate claim Lzimv: PNo_strict_imv L' R' (SNoLev z) (λγ ⇒ γ ∈ z).
We will prove PNo_strict_upperbd L' (SNoLev z) (λγ ⇒ γ ∈ z) ∧ PNo_strict_lowerbd R' (SNoLev z) (λγ ⇒ γ ∈ z).
Apply andI to the current goal.
Let γ be given.
Assume Hc: ordinal γ.
Let q be given.
Assume Hq: L' γ q.
We will prove PNoLt γ q (SNoLev z) (λγ ⇒ γ ∈ z).
Apply Hq to the current goal.
Assume Hq1: ordinal γ.
Assume Hq2: PSNo γ q ∈ L.
Apply SNoLt_PSNo_PNoLt γ (SNoLev z) q (λγ ⇒ γ ∈ z) Hc LLz to the current goal.
We will prove PSNo γ q < PSNo (SNoLev z) (λγ ⇒ γ ∈ z).
rewrite the current goal using SNo_PSNo_eta z Hz (from right to left).
We will prove PSNo γ q < z.
An exact proof term for the current goal is H10 (PSNo γ q) Hq2.
Let γ be given.
Assume Hc: ordinal γ.
Let q be given.
Assume Hq: R' γ q.
We will prove PNoLt (SNoLev z) (λγ ⇒ γ ∈ z) γ q.
Apply Hq to the current goal.
Assume Hq1: ordinal γ.
Assume Hq2: PSNo γ q ∈ R.
Apply SNoLt_PSNo_PNoLt (SNoLev z) γ (λγ ⇒ γ ∈ z) q LLz Hc to the current goal.
We will prove PSNo (SNoLev z) (λγ ⇒ γ ∈ z) < PSNo γ q.
rewrite the current goal using SNo_PSNo_eta z Hz (from right to left).
We will prove z < PSNo γ q.
An exact proof term for the current goal is H11 (PSNo γ q) Hq2.
We prove the intermediate claim LLznt: SNoLev z ∉ tau.
Assume H12: SNoLev z ∈ tau.
An exact proof term for the current goal is H3 (SNoLev z) H12 (λγ ⇒ γ ∈ z) Lzimv.
We prove the intermediate claim LLzlet: tau ⊆ SNoLev z.
Apply ordinal_In_Or_Subq (SNoLev z) tau LLz H1 to the current goal.
Assume H12: SNoLev z ∈ tau.
We will prove False.
An exact proof term for the current goal is LLznt H12.
Assume H12.
An exact proof term for the current goal is H12.
We will prove SNoLev (SNoCut L R) ⊆ SNoLev z ∧ PNoEq_ (SNoLev (SNoCut L R)) (λγ ⇒ γ ∈ SNoCut L R) (λγ ⇒ γ ∈ z).
rewrite the current goal using LLleveqtau (from left to right).
We will prove tau ⊆ SNoLev z ∧ PNoEq_ tau (λγ ⇒ γ ∈ SNoCut L R) (λγ ⇒ γ ∈ z).
Apply andI to the current goal.
We will prove tau ⊆ SNoLev z.
An exact proof term for the current goal is LLzlet.
We will prove PNoEq_ tau (λγ ⇒ γ ∈ SNoCut L R) (λγ ⇒ γ ∈ z).
Apply PNoLt_trichotomy_or_ w (λγ ⇒ γ ∈ z) tau H1 to the current goal.
Assume H12.
Apply H12 to the current goal.
Assume H12: PNoLt_ tau w (λγ ⇒ γ ∈ z).
We will prove False.
Apply H12 to the current goal.
Let δ be given.
Assume H13.
Apply H13 to the current goal.
Assume Hd: δ ∈ tau.
Assume H13.
Apply H13 to the current goal.
Assume H13.
Apply H13 to the current goal.
Assume H13: PNoEq_ δ w (λγ ⇒ γ ∈ z).
Assume H14: ¬ w δ.
Assume H15: δ ∈ z.
We prove the intermediate claim Ld: ordinal δ.
An exact proof term for the current goal is ordinal_Hered tau H1 δ Hd.
We prove the intermediate claim Lsd: ordinal (ordsucc δ).
An exact proof term for the current goal is ordinal_ordsucc δ Ld.
Set z0 to be the term λeps ⇒ eps ∈ z ∧ eps ≠ δ of type set → prop.
Set z1 to be the term λeps ⇒ eps ∈ z ∨ eps = δ of type set → prop.
We prove the intermediate claim Lnz0d: ¬ z0 δ.
Assume H10.
Apply H10 to the current goal.
Assume H11: δ ∈ z.
Assume H12: δ ≠ δ.
Apply H12 to the current goal.
Use reflexivity.
We prove the intermediate claim Lz1d: z1 δ.
We will prove δ ∈ z ∨ δ = δ.
Apply orIR to the current goal.
Use reflexivity.
Apply H3 δ Hd (λγ ⇒ γ ∈ z) to the current goal.
We will prove PNo_strict_imv L' R' δ (λγ ⇒ γ ∈ z).
Apply PNo_rel_split_imv_imp_strict_imv L' R' δ Ld (λγ ⇒ γ ∈ z) to the current goal.
We will prove PNo_rel_strict_split_imv L' R' δ (λγ ⇒ γ ∈ z).
We will prove PNo_rel_strict_imv L' R' (ordsucc δ) z0 ∧ PNo_rel_strict_imv L' R' (ordsucc δ) z1.
Apply andI to the current goal.
We will prove PNo_rel_strict_imv L' R' (ordsucc δ) z0.
Apply PNoEq_rel_strict_imv L' R' (ordsucc δ) Lsd w z0 to the current goal.
We will prove PNoEq_ (ordsucc δ) w z0.
Let eps be given.
Assume He: eps ∈ ordsucc δ.
Apply ordsuccE δ eps He to the current goal.
Assume He1: eps ∈ δ.
Apply iff_trans (w eps) (eps ∈ z) (z0 eps) to the current goal.
An exact proof term for the current goal is H13 eps He1.
An exact proof term for the current goal is PNo_extend0_eq δ (λγ ⇒ γ ∈ z) eps He1.
Assume He1: eps = δ.
We will prove w eps ↔ z0 eps.
rewrite the current goal using He1 (from left to right).
We will prove w δ ↔ z0 δ.
Apply iffI to the current goal.
Assume H16: w δ.
We will prove False.
An exact proof term for the current goal is H14 H16.
Assume H16: z0 δ.
We will prove False.
An exact proof term for the current goal is Lnz0d H16.
We will prove PNo_rel_strict_imv L' R' (ordsucc δ) w.
Apply PNo_strict_imv_imp_rel_strict_imv L' R' tau H1 (ordsucc δ) to the current goal.
We will prove ordsucc δ ∈ ordsucc tau.
Apply ordinal_ordsucc_In tau H1 to the current goal.
An exact proof term for the current goal is Hd.
We will prove PNo_strict_imv L' R' tau w.
An exact proof term for the current goal is H2.
We will prove PNo_rel_strict_imv L' R' (ordsucc δ) z1.
Apply PNoEq_rel_strict_imv L' R' (ordsucc δ) Lsd (λγ ⇒ γ ∈ z) z1 to the current goal.
We will prove PNoEq_ (ordsucc δ) (λγ ⇒ γ ∈ z) z1.
Let eps be given.
Assume He: eps ∈ ordsucc δ.
Apply ordsuccE δ eps He to the current goal.
Assume He1: eps ∈ δ.
An exact proof term for the current goal is PNo_extend1_eq δ (λγ ⇒ γ ∈ z) eps He1.
Assume He1: eps = δ.
We will prove eps ∈ z ↔ z1 eps.
rewrite the current goal using He1 (from left to right).
We will prove δ ∈ z ↔ z1 δ.
Apply iffI to the current goal.
Assume _.
An exact proof term for the current goal is Lz1d.
Assume _.
An exact proof term for the current goal is H15.
We will prove PNo_rel_strict_imv L' R' (ordsucc δ) (λγ ⇒ γ ∈ z).
Apply PNo_strict_imv_imp_rel_strict_imv L' R' (SNoLev z) LLz (ordsucc δ) to the current goal.
We will prove ordsucc δ ∈ ordsucc (SNoLev z).
Apply ordinal_ordsucc_In (SNoLev z) LLz to the current goal.
We will prove δ ∈ SNoLev z.
Apply LLzlet to the current goal.
We will prove δ ∈ tau.
An exact proof term for the current goal is Hd.
We will prove PNo_strict_imv L' R' (SNoLev z) (λγ ⇒ γ ∈ z).
An exact proof term for the current goal is Lzimv.
Assume H12: PNoEq_ tau w (λγ ⇒ γ ∈ z).
Apply PNoEq_tra_ tau (λγ ⇒ γ ∈ SNoCut L R) w (λγ ⇒ γ ∈ z) to the current goal.
We will prove PNoEq_ tau (λγ ⇒ γ ∈ SNoCut L R) w.
An exact proof term for the current goal is LLecw.
We will prove PNoEq_ tau w (λγ ⇒ γ ∈ z).
An exact proof term for the current goal is H12.
Assume H12: PNoLt_ tau (λγ ⇒ γ ∈ z) w.
We will prove False.
Apply H12 to the current goal.
Let δ be given.
Assume H13.
Apply H13 to the current goal.
Assume Hd: δ ∈ tau.
Assume H13.
Apply H13 to the current goal.
Assume H13.
Apply H13 to the current goal.
Assume H13: PNoEq_ δ (λγ ⇒ γ ∈ z) w.
Assume H14: δ ∉ z.
Assume H15: w δ.
We prove the intermediate claim Ld: ordinal δ.
An exact proof term for the current goal is ordinal_Hered tau H1 δ Hd.
We prove the intermediate claim Lsd: ordinal (ordsucc δ).
An exact proof term for the current goal is ordinal_ordsucc δ Ld.
Set z0 to be the term λeps ⇒ eps ∈ z ∧ eps ≠ δ of type set → prop.
Set z1 to be the term λeps ⇒ eps ∈ z ∨ eps = δ of type set → prop.
We prove the intermediate claim Lnz0d: ¬ z0 δ.
Assume H10.
Apply H10 to the current goal.
Assume H11: δ ∈ z.
Assume H12: δ ≠ δ.
Apply H12 to the current goal.
Use reflexivity.
We prove the intermediate claim Lz1d: z1 δ.
We will prove δ ∈ z ∨ δ = δ.
Apply orIR to the current goal.
Use reflexivity.
Apply H3 δ Hd (λγ ⇒ γ ∈ z) to the current goal.
We will prove PNo_strict_imv L' R' δ (λγ ⇒ γ ∈ z).
Apply PNo_rel_split_imv_imp_strict_imv L' R' δ Ld (λγ ⇒ γ ∈ z) to the current goal.
We will prove PNo_rel_strict_split_imv L' R' δ (λγ ⇒ γ ∈ z).
We will prove PNo_rel_strict_imv L' R' (ordsucc δ) z0 ∧ PNo_rel_strict_imv L' R' (ordsucc δ) z1.
Apply andI to the current goal.
We will prove PNo_rel_strict_imv L' R' (ordsucc δ) z0.
Apply PNoEq_rel_strict_imv L' R' (ordsucc δ) Lsd (λγ ⇒ γ ∈ z) z0 to the current goal.
We will prove PNoEq_ (ordsucc δ) (λγ ⇒ γ ∈ z) z0.
Let eps be given.
Assume He: eps ∈ ordsucc δ.
Apply ordsuccE δ eps He to the current goal.
Assume He1: eps ∈ δ.
An exact proof term for the current goal is PNo_extend0_eq δ (λγ ⇒ γ ∈ z) eps He1.
Assume He1: eps = δ.
We will prove eps ∈ z ↔ z0 eps.
rewrite the current goal using He1 (from left to right).
We will prove δ ∈ z ↔ z0 δ.
Apply iffI to the current goal.
Assume H16: δ ∈ z.
We will prove False.
An exact proof term for the current goal is H14 H16.
Assume H16: z0 δ.
We will prove False.
An exact proof term for the current goal is Lnz0d H16.
We will prove PNo_rel_strict_imv L' R' (ordsucc δ) (λγ ⇒ γ ∈ z).
Apply PNo_strict_imv_imp_rel_strict_imv L' R' (SNoLev z) LLz (ordsucc δ) to the current goal.
We will prove ordsucc δ ∈ ordsucc (SNoLev z).
Apply ordinal_ordsucc_In (SNoLev z) LLz to the current goal.
We will prove δ ∈ SNoLev z.
Apply LLzlet to the current goal.
We will prove δ ∈ tau.
An exact proof term for the current goal is Hd.
We will prove PNo_strict_imv L' R' (SNoLev z) (λγ ⇒ γ ∈ z).
An exact proof term for the current goal is Lzimv.
We will prove PNo_rel_strict_imv L' R' (ordsucc δ) z1.
Apply PNoEq_rel_strict_imv L' R' (ordsucc δ) Lsd w z1 to the current goal.
We will prove PNoEq_ (ordsucc δ) w z1.
Let eps be given.
Assume He: eps ∈ ordsucc δ.
Apply ordsuccE δ eps He to the current goal.
Assume He1: eps ∈ δ.
Apply iff_trans (w eps) (eps ∈ z) (z1 eps) to the current goal.
Apply iff_sym to the current goal.
An exact proof term for the current goal is H13 eps He1.
An exact proof term for the current goal is PNo_extend1_eq δ (λγ ⇒ γ ∈ z) eps He1.
Assume He1: eps = δ.
We will prove w eps ↔ z1 eps.
rewrite the current goal using He1 (from left to right).
We will prove w δ ↔ z1 δ.
Apply iffI to the current goal.
Assume _.
An exact proof term for the current goal is Lz1d.
Assume _.
An exact proof term for the current goal is H15.
We will prove PNo_rel_strict_imv L' R' (ordsucc δ) w.
Apply PNo_strict_imv_imp_rel_strict_imv L' R' tau H1 (ordsucc δ) to the current goal.
We will prove ordsucc δ ∈ ordsucc tau.
Apply ordinal_ordsucc_In tau H1 to the current goal.
An exact proof term for the current goal is Hd.
We will prove PNo_strict_imv L' R' tau w.
An exact proof term for the current goal is H2.
∎