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 λalpha p ⇒ ordinal alpha ∧ PSNo alpha p ∈ L of type set → (set → prop) → prop.
Set R' to be the term λalpha p ⇒ ordinal alpha ∧ PSNo alpha 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 (alpha ∪ beta) ∧ (∀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)) (λgamma ⇒ gamma ∈ SNoCut L R) (λgamma ⇒ gamma ∈ z)).
We prove the intermediate claim LLR: PNoLt_pwise L' R'.
Let gamma be given.
Assume Hc: ordinal gamma.
Let p be given.
Assume H1: L' gamma p.
Apply H1 to the current goal.
Assume _ H1.
Let delta be given.
Assume Hd: ordinal delta.
Let q be given.
Assume H2: R' delta q.
Apply H2 to the current goal.
Assume _ H2.
We will prove PNoLt gamma p delta q.
Apply SNoLt_PSNo_PNoLt gamma delta p q Hc Hd to the current goal.
We will prove PSNo gamma p < PSNo delta q.
An exact proof term for the current goal is HLR (PSNo gamma p) H1 (PSNo delta q) H2.
We prove the intermediate claim La: ordinal alpha.
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 beta.
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 (alpha ∪ beta).
Apply ordinal_linear alpha beta La Lb to the current goal.
We will prove alpha ⊆ beta → ordinal (alpha ∪ beta).
rewrite the current goal using Subq_binunion_eq alpha beta (from left to right).
We will prove alpha ∪ beta = beta → ordinal (alpha ∪ beta).
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 beta ⊆ alpha → ordinal (alpha ∪ beta).
rewrite the current goal using Subq_binunion_eq beta alpha (from left to right).
We will prove beta ∪ alpha = alpha → ordinal (alpha ∪ beta).
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 (alpha ∪ beta) L'.
Let gamma be given.
Let p be given.
Assume H1.
Apply H1 to the current goal.
Assume H1: ordinal gamma.
Assume H2: PSNo gamma p ∈ L.
We will prove gamma ∈ alpha ∪ beta.
Apply binunionI1 to the current goal.
We will prove gamma ∈ ⋃x ∈ Lordsucc (SNoLev x).
Apply famunionI L (λx ⇒ ordsucc (SNoLev x)) (PSNo gamma p) gamma to the current goal.
We will prove PSNo gamma p ∈ L.
An exact proof term for the current goal is H2.
We will prove gamma ∈ ordsucc (SNoLev (PSNo gamma p)).
rewrite the current goal using SNoLev_PSNo gamma H1 p (from left to right).
We will prove gamma ∈ ordsucc gamma.
Apply ordsuccI2 to the current goal.
We prove the intermediate claim LRab: PNo_lenbdd (alpha ∪ beta) R'.
Let gamma be given.
Let p be given.
Assume H1.
Apply H1 to the current goal.
Assume H1: ordinal gamma.
Assume H2: PSNo gamma p ∈ R.
We will prove gamma ∈ alpha ∪ beta.
Apply binunionI2 to the current goal.
We will prove gamma ∈ ⋃y ∈ Rordsucc (SNoLev y).
Apply famunionI R (λy ⇒ ordsucc (SNoLev y)) (PSNo gamma p) gamma to the current goal.
We will prove PSNo gamma p ∈ R.
An exact proof term for the current goal is H2.
We will prove gamma ∈ ordsucc (SNoLev (PSNo gamma p)).
rewrite the current goal using SNoLev_PSNo gamma H1 p (from left to right).
We will prove gamma ∈ ordsucc gamma.
Apply ordsuccI2 to the current goal.
Apply PNo_bd_pred L' R' LLR (alpha ∪ beta) 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: ∀gamma ∈ tau, ∀q : set → prop, ¬ PNo_strict_imv L' R' gamma 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 ∃alpha, ordinal alpha ∧ SNo_ alpha (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 (alpha ∪ beta).
An exact proof term for the current goal is PNo_bd_In L' R' LLR (alpha ∪ beta) Lab LLab LRab.
We prove the intermediate claim LLbd: SNoLev (SNoCut L R) ∈ ordsucc (alpha ∪ beta).
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 (λgamma ⇒ gamma ∈ SNoCut L R) w.
We will prove PNoEq_ tau (λgamma ⇒ gamma ∈ 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) (λgamma ⇒ gamma ∈ 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) (λgamma ⇒ gamma ∈ x).
We will prove ordinal (SNoLev x) ∧ PSNo (SNoLev x) (λgamma ⇒ gamma ∈ 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 (λgamma ⇒ gamma ∈ x) w LLx H1 to the current goal.
We will prove PNoLt (SNoLev x) (λgamma ⇒ gamma ∈ x) tau w.
An exact proof term for the current goal is H4 (SNoLev x) LLx (λgamma ⇒ gamma ∈ 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) (λgamma ⇒ gamma ∈ 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) (λgamma ⇒ gamma ∈ y).
We will prove ordinal (SNoLev y) ∧ PSNo (SNoLev y) (λgamma ⇒ gamma ∈ 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 (λgamma ⇒ gamma ∈ y) H1 LLy to the current goal.
We will prove PNoLt tau w (SNoLev y) (λgamma ⇒ gamma ∈ y).
An exact proof term for the current goal is H5 (SNoLev y) LLy (λgamma ⇒ gamma ∈ 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)) (λgamma ⇒ gamma ∈ SNoCut L R) (λgamma ⇒ gamma ∈ 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) (λgamma ⇒ gamma ∈ z).
We will prove PNo_strict_upperbd L' (SNoLev z) (λgamma ⇒ gamma ∈ z) ∧ PNo_strict_lowerbd R' (SNoLev z) (λgamma ⇒ gamma ∈ z).
Apply andI to the current goal.
Let gamma be given.
Assume Hc: ordinal gamma.
Let q be given.
Assume Hq: L' gamma q.
We will prove PNoLt gamma q (SNoLev z) (λgamma ⇒ gamma ∈ z).
Apply Hq to the current goal.
Assume Hq1: ordinal gamma.
Assume Hq2: PSNo gamma q ∈ L.
Apply SNoLt_PSNo_PNoLt gamma (SNoLev z) q (λgamma ⇒ gamma ∈ z) Hc LLz to the current goal.
We will prove PSNo gamma q < PSNo (SNoLev z) (λgamma ⇒ gamma ∈ z).
rewrite the current goal using SNo_PSNo_eta z Hz (from right to left).
We will prove PSNo gamma q < z.
An exact proof term for the current goal is H10 (PSNo gamma q) Hq2.
Let gamma be given.
Assume Hc: ordinal gamma.
Let q be given.
Assume Hq: R' gamma q.
We will prove PNoLt (SNoLev z) (λgamma ⇒ gamma ∈ z) gamma q.
Apply Hq to the current goal.
Assume Hq1: ordinal gamma.
Assume Hq2: PSNo gamma q ∈ R.
Apply SNoLt_PSNo_PNoLt (SNoLev z) gamma (λgamma ⇒ gamma ∈ z) q LLz Hc to the current goal.
We will prove PSNo (SNoLev z) (λgamma ⇒ gamma ∈ z) < PSNo gamma q.
rewrite the current goal using SNo_PSNo_eta z Hz (from right to left).
We will prove z < PSNo gamma q.
An exact proof term for the current goal is H11 (PSNo gamma 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 (λgamma ⇒ gamma ∈ 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)) (λgamma ⇒ gamma ∈ SNoCut L R) (λgamma ⇒ gamma ∈ z).
rewrite the current goal using LLleveqtau (from left to right).
We will prove tau ⊆ SNoLev z ∧ PNoEq_ tau (λgamma ⇒ gamma ∈ SNoCut L R) (λgamma ⇒ gamma ∈ 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 (λgamma ⇒ gamma ∈ SNoCut L R) (λgamma ⇒ gamma ∈ z).
Apply PNoLt_trichotomy_or_ w (λgamma ⇒ gamma ∈ z) tau H1 to the current goal.
Assume H12.
Apply H12 to the current goal.
Assume H12: PNoLt_ tau w (λgamma ⇒ gamma ∈ z).
We will prove False.
Apply H12 to the current goal.
Let delta be given.
Assume H13.
Apply H13 to the current goal.
Assume Hd: delta ∈ tau.
Assume H13.
Apply H13 to the current goal.
Assume H13.
Apply H13 to the current goal.
Assume H13: PNoEq_ delta w (λgamma ⇒ gamma ∈ z).
Assume H14: ¬ w delta.
Assume H15: delta ∈ z.
We prove the intermediate claim Ld: ordinal delta.
An exact proof term for the current goal is ordinal_Hered tau H1 delta Hd.
We prove the intermediate claim Lsd: ordinal (ordsucc delta).
An exact proof term for the current goal is ordinal_ordsucc delta Ld.
Set z0 to be the term λeps ⇒ eps ∈ z ∧ eps ≠ delta of type set → prop.
Set z1 to be the term λeps ⇒ eps ∈ z ∨ eps = delta of type set → prop.
We prove the intermediate claim Lnz0d: ¬ z0 delta.
Assume H10.
Apply H10 to the current goal.
Assume H11: delta ∈ z.
Assume H12: delta ≠ delta.
Apply H12 to the current goal.
Use reflexivity.
We prove the intermediate claim Lz1d: z1 delta.
We will prove delta ∈ z ∨ delta = delta.
Apply orIR to the current goal.
Use reflexivity.
Apply H3 delta Hd (λgamma ⇒ gamma ∈ z) to the current goal.
We will prove PNo_strict_imv L' R' delta (λgamma ⇒ gamma ∈ z).
Apply PNo_rel_split_imv_imp_strict_imv L' R' delta Ld (λgamma ⇒ gamma ∈ z) to the current goal.
We will prove PNo_rel_strict_split_imv L' R' delta (λgamma ⇒ gamma ∈ z).
We will prove PNo_rel_strict_imv L' R' (ordsucc delta) z0 ∧ PNo_rel_strict_imv L' R' (ordsucc delta) z1.
Apply andI to the current goal.
We will prove PNo_rel_strict_imv L' R' (ordsucc delta) z0.
Apply PNoEq_rel_strict_imv L' R' (ordsucc delta) Lsd w z0 to the current goal.
We will prove PNoEq_ (ordsucc delta) w z0.
Let eps be given.
Assume He: eps ∈ ordsucc delta.
Apply ordsuccE delta eps He to the current goal.
Assume He1: eps ∈ delta.
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 delta (λgamma ⇒ gamma ∈ z) eps He1.
Assume He1: eps = delta.
We will prove w eps ↔ z0 eps.
rewrite the current goal using He1 (from left to right).
We will prove w delta ↔ z0 delta.
Apply iffI to the current goal.
Assume H16: w delta.
We will prove False.
An exact proof term for the current goal is H14 H16.
Assume H16: z0 delta.
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 delta) w.
Apply PNo_strict_imv_imp_rel_strict_imv L' R' tau H1 (ordsucc delta) to the current goal.
We will prove ordsucc delta ∈ 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 delta) z1.
Apply PNoEq_rel_strict_imv L' R' (ordsucc delta) Lsd (λgamma ⇒ gamma ∈ z) z1 to the current goal.
We will prove PNoEq_ (ordsucc delta) (λgamma ⇒ gamma ∈ z) z1.
Let eps be given.
Assume He: eps ∈ ordsucc delta.
Apply ordsuccE delta eps He to the current goal.
Assume He1: eps ∈ delta.
An exact proof term for the current goal is PNo_extend1_eq delta (λgamma ⇒ gamma ∈ z) eps He1.
Assume He1: eps = delta.
We will prove eps ∈ z ↔ z1 eps.
rewrite the current goal using He1 (from left to right).
We will prove delta ∈ z ↔ z1 delta.
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 delta) (λgamma ⇒ gamma ∈ z).
Apply PNo_strict_imv_imp_rel_strict_imv L' R' (SNoLev z) LLz (ordsucc delta) to the current goal.
We will prove ordsucc delta ∈ ordsucc (SNoLev z).
Apply ordinal_ordsucc_In (SNoLev z) LLz to the current goal.
We will prove delta ∈ SNoLev z.
Apply LLzlet to the current goal.
We will prove delta ∈ tau.
An exact proof term for the current goal is Hd.
We will prove PNo_strict_imv L' R' (SNoLev z) (λgamma ⇒ gamma ∈ z).
An exact proof term for the current goal is Lzimv.
Assume H12: PNoEq_ tau w (λgamma ⇒ gamma ∈ z).
Apply PNoEq_tra_ tau (λgamma ⇒ gamma ∈ SNoCut L R) w (λgamma ⇒ gamma ∈ z) to the current goal.
We will prove PNoEq_ tau (λgamma ⇒ gamma ∈ SNoCut L R) w.
An exact proof term for the current goal is LLecw.
We will prove PNoEq_ tau w (λgamma ⇒ gamma ∈ z).
An exact proof term for the current goal is H12.
Assume H12: PNoLt_ tau (λgamma ⇒ gamma ∈ z) w.
We will prove False.
Apply H12 to the current goal.
Let delta be given.
Assume H13.
Apply H13 to the current goal.
Assume Hd: delta ∈ tau.
Assume H13.
Apply H13 to the current goal.
Assume H13.
Apply H13 to the current goal.
Assume H13: PNoEq_ delta (λgamma ⇒ gamma ∈ z) w.
Assume H14: delta ∉ z.
Assume H15: w delta.
We prove the intermediate claim Ld: ordinal delta.
An exact proof term for the current goal is ordinal_Hered tau H1 delta Hd.
We prove the intermediate claim Lsd: ordinal (ordsucc delta).
An exact proof term for the current goal is ordinal_ordsucc delta Ld.
Set z0 to be the term λeps ⇒ eps ∈ z ∧ eps ≠ delta of type set → prop.
Set z1 to be the term λeps ⇒ eps ∈ z ∨ eps = delta of type set → prop.
We prove the intermediate claim Lnz0d: ¬ z0 delta.
Assume H10.
Apply H10 to the current goal.
Assume H11: delta ∈ z.
Assume H12: delta ≠ delta.
Apply H12 to the current goal.
Use reflexivity.
We prove the intermediate claim Lz1d: z1 delta.
We will prove delta ∈ z ∨ delta = delta.
Apply orIR to the current goal.
Use reflexivity.
Apply H3 delta Hd (λgamma ⇒ gamma ∈ z) to the current goal.
We will prove PNo_strict_imv L' R' delta (λgamma ⇒ gamma ∈ z).
Apply PNo_rel_split_imv_imp_strict_imv L' R' delta Ld (λgamma ⇒ gamma ∈ z) to the current goal.
We will prove PNo_rel_strict_split_imv L' R' delta (λgamma ⇒ gamma ∈ z).
We will prove PNo_rel_strict_imv L' R' (ordsucc delta) z0 ∧ PNo_rel_strict_imv L' R' (ordsucc delta) z1.
Apply andI to the current goal.
We will prove PNo_rel_strict_imv L' R' (ordsucc delta) z0.
Apply PNoEq_rel_strict_imv L' R' (ordsucc delta) Lsd (λgamma ⇒ gamma ∈ z) z0 to the current goal.
We will prove PNoEq_ (ordsucc delta) (λgamma ⇒ gamma ∈ z) z0.
Let eps be given.
Assume He: eps ∈ ordsucc delta.
Apply ordsuccE delta eps He to the current goal.
Assume He1: eps ∈ delta.
An exact proof term for the current goal is PNo_extend0_eq delta (λgamma ⇒ gamma ∈ z) eps He1.
Assume He1: eps = delta.
We will prove eps ∈ z ↔ z0 eps.
rewrite the current goal using He1 (from left to right).
We will prove delta ∈ z ↔ z0 delta.
Apply iffI to the current goal.
Assume H16: delta ∈ z.
We will prove False.
An exact proof term for the current goal is H14 H16.
Assume H16: z0 delta.
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 delta) (λgamma ⇒ gamma ∈ z).
Apply PNo_strict_imv_imp_rel_strict_imv L' R' (SNoLev z) LLz (ordsucc delta) to the current goal.
We will prove ordsucc delta ∈ ordsucc (SNoLev z).
Apply ordinal_ordsucc_In (SNoLev z) LLz to the current goal.
We will prove delta ∈ SNoLev z.
Apply LLzlet to the current goal.
We will prove delta ∈ tau.
An exact proof term for the current goal is Hd.
We will prove PNo_strict_imv L' R' (SNoLev z) (λgamma ⇒ gamma ∈ z).
An exact proof term for the current goal is Lzimv.
We will prove PNo_rel_strict_imv L' R' (ordsucc delta) z1.
Apply PNoEq_rel_strict_imv L' R' (ordsucc delta) Lsd w z1 to the current goal.
We will prove PNoEq_ (ordsucc delta) w z1.
Let eps be given.
Assume He: eps ∈ ordsucc delta.
Apply ordsuccE delta eps He to the current goal.
Assume He1: eps ∈ delta.
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 delta (λgamma ⇒ gamma ∈ z) eps He1.
Assume He1: eps = delta.
We will prove w eps ↔ z1 eps.
rewrite the current goal using He1 (from left to right).
We will prove w delta ↔ z1 delta.
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 delta) w.
Apply PNo_strict_imv_imp_rel_strict_imv L' R' tau H1 (ordsucc delta) to the current goal.
We will prove ordsucc delta ∈ 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.
∎