Let L and R be given.
Let alpha be given.
Assume Ha.
Apply Ha to the current goal.
Assume Ha1 _.
Assume HaL HaR.
Let p be given.
Assume Hp1: PNo_rel_strict_imv L R alpha p.
Apply Hp1 to the current goal.
Assume Hp1a Hp1b.
Set p1 to be the term λdelta ⇒ p delta ∨ delta = alpha of type set → prop.
We prove the intermediate claim Lsa: ordinal (ordsucc alpha).
An exact proof term for the current goal is ordinal_ordsucc alpha Ha.
We prove the intermediate claim Lpp1e: PNoEq_ alpha p p1.
An exact proof term for the current goal is PNo_extend1_eq alpha p.
We will prove PNo_rel_strict_upperbd L (ordsucc alpha) p1 ∧ PNo_rel_strict_lowerbd R (ordsucc alpha) p1.
Apply andI to the current goal.
We will prove PNo_rel_strict_upperbd L (ordsucc alpha) p1.
Let gamma be given.
Assume Hc: gamma ∈ ordsucc alpha.
Let q be given.
Assume Hq: PNo_downc L gamma q.
We prove the intermediate claim Lc: ordinal gamma.
An exact proof term for the current goal is ordinal_Hered (ordsucc alpha) Lsa gamma Hc.
We will prove PNoLt gamma q (ordsucc alpha) p1.
Apply PNoLt_tra gamma alpha (ordsucc alpha) Lc Ha Lsa q p p1 to the current goal.
We will prove PNoLt gamma q alpha p.
Apply Hq to the current goal.
Let delta be given.
Assume Hq1.
Apply Hq1 to the current goal.
Assume Hd: ordinal delta.
Assume Hq1.
Apply Hq1 to the current goal.
Let r be given.
Assume Hq1.
Apply Hq1 to the current goal.
Assume Hr: L delta r.
Assume Hqr: PNoLe gamma q delta r.
We prove the intermediate claim Ldr: PNo_downc L delta r.
We will prove ∃beta, ordinal beta ∧ ∃q : set → prop, L beta q ∧ PNoLe delta r beta q.
We use delta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hd.
We use r to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hr.
Apply PNoLe_ref to the current goal.
Apply PNoLeLt_tra gamma delta alpha Lc Hd Ha q r p Hqr to the current goal.
We will prove PNoLt delta r alpha p.
An exact proof term for the current goal is Hp1a delta (HaL delta r Hr) r Ldr.
We will prove PNoLt alpha p (ordsucc alpha) p1.
Apply PNoLtI2 to the current goal.
We will prove alpha ∈ ordsucc alpha.
Apply ordsuccI2 to the current goal.
We will prove PNoEq_ alpha p p1.
An exact proof term for the current goal is Lpp1e.
We will prove p1 alpha.
We will prove p alpha ∨ alpha = alpha.
Apply orIR to the current goal.
Use reflexivity.
We will prove PNo_rel_strict_lowerbd R (ordsucc alpha) p1.
Let gamma be given.
Assume Hc: gamma ∈ ordsucc alpha.
Let q be given.
Assume Hq: PNo_upc R gamma q.
We prove the intermediate claim Lc: ordinal gamma.
An exact proof term for the current goal is ordinal_Hered (ordsucc alpha) Lsa gamma Hc.
We will prove PNoLt (ordsucc alpha) p1 gamma q.
Apply Hq to the current goal.
Let delta be given.
Assume Hq1.
Apply Hq1 to the current goal.
Assume Hd: ordinal delta.
Assume Hq1.
Apply Hq1 to the current goal.
Let r be given.
Assume Hq1.
Apply Hq1 to the current goal.
Assume Hr: R delta r.
Assume Hrq: PNoLe delta r gamma q.
Apply (λH : PNoLt (ordsucc alpha) p1 delta r ⇒ PNoLtLe_tra (ordsucc alpha) delta gamma Lsa Hd Lc p1 r q H Hrq) to the current goal.
We will prove PNoLt (ordsucc alpha) p1 delta r.
We prove the intermediate claim Lda: delta ∈ alpha.
An exact proof term for the current goal is HaR delta r Hr.
We prove the intermediate claim Ldsa: delta ∈ ordsucc alpha.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Lda.
We prove the intermediate claim Ldr: PNo_upc R delta r.
We will prove ∃beta, ordinal beta ∧ ∃q : set → prop, R beta q ∧ PNoLe beta q delta r.
We use delta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hd.
We use r to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hr.
Apply PNoLe_ref to the current goal.
We prove the intermediate claim Lpr: PNoLt alpha p delta r.
An exact proof term for the current goal is Hp1b delta Lda r Ldr.
Apply PNoLt_trichotomy_or delta (ordsucc alpha) r p1 Hd Lsa to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: PNoLt delta r (ordsucc alpha) p1.
We will prove False.
Apply PNoLt_irref alpha p to the current goal.
We will prove PNoLt alpha p alpha p.
Apply PNoLt_tra alpha delta alpha Ha Hd Ha p r p Lpr to the current goal.
We will prove PNoLt delta r alpha p.
Apply PNoLtE delta (ordsucc alpha) r p1 H1 to the current goal.
Assume H2: PNoLt_ (delta ∩ ordsucc alpha) r p1.
Apply H2 to the current goal.
Let eps be given.
Assume H3.
Apply H3 to the current goal.
Assume He: eps ∈ delta ∩ ordsucc alpha.
Apply binintersectE delta (ordsucc alpha) eps He to the current goal.
Assume He1 He2.
We prove the intermediate claim Lea: eps ∈ alpha.
An exact proof term for the current goal is Ha1 delta Lda eps He1.
Assume H3.
Apply H3 to the current goal.
Assume H3.
Apply H3 to the current goal.
Assume H3: PNoEq_ eps r p1.
Assume H4: ¬ r eps.
Assume H5: p1 eps.
Apply PNoLtI1 to the current goal.
We will prove PNoLt_ (delta ∩ alpha) r p.
We will prove ∃beta ∈ delta ∩ alpha, PNoEq_ beta r p ∧ ¬ r beta ∧ p beta.
We use eps to witness the existential quantifier.
Apply andI to the current goal.
We will prove eps ∈ delta ∩ alpha.
Apply binintersectI to the current goal.
An exact proof term for the current goal is He1.
An exact proof term for the current goal is Lea.
Apply and3I to the current goal.
We will prove PNoEq_ eps r p.
Apply PNoEq_tra_ eps r p1 p to the current goal.
An exact proof term for the current goal is H3.
Apply PNoEq_antimon_ p1 p alpha Ha eps Lea to the current goal.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is Lpp1e.
We will prove ¬ r eps.
An exact proof term for the current goal is H4.
We will prove p eps.
Apply H5 to the current goal.
An exact proof term for the current goal is (λH ⇒ H).
Assume H6: eps = alpha.
We will prove False.
Apply In_irref alpha to the current goal.
rewrite the current goal using H6 (from right to left) at position 1.
An exact proof term for the current goal is Lea.
Assume H2: delta ∈ ordsucc alpha.
Assume H3: PNoEq_ delta r p1.
Assume H4: p1 delta.
Apply PNoLtI2 delta alpha r p Lda to the current goal.
We will prove PNoEq_ delta r p.
Apply PNoEq_tra_ delta r p1 p to the current goal.
An exact proof term for the current goal is H3.
Apply PNoEq_antimon_ p1 p alpha Ha delta Lda to the current goal.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is Lpp1e.
We will prove p delta.
Apply H4 to the current goal.
An exact proof term for the current goal is (λH ⇒ H).
Assume H5: delta = alpha.
We will prove False.
Apply In_irref alpha to the current goal.
rewrite the current goal using H5 (from right to left) at position 1.
An exact proof term for the current goal is Lda.
Assume H2: ordsucc alpha ∈ delta.
We will prove False.
An exact proof term for the current goal is In_no2cycle delta (ordsucc alpha) Ldsa H2.
Assume H1.
Apply H1 to the current goal.
Assume H2: delta = ordsucc alpha.
We will prove False.
Apply In_irref delta to the current goal.
rewrite the current goal using H2 (from left to right) at position 2.
An exact proof term for the current goal is Ldsa.
Assume H1.
An exact proof term for the current goal is H1.
∎