Let L and R be given.
Let α 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 α p.
Apply Hp1 to the current goal.
Assume Hp1a Hp1b.
Set p1 to be the term λδ ⇒ p δ ∨ δ = α of type set → prop.
We prove the intermediate claim Lsa: ordinal (ordsucc α).
An exact proof term for the current goal is ordinal_ordsucc α Ha.
We prove the intermediate claim Lpp1e: PNoEq_ α p p1.
An exact proof term for the current goal is PNo_extend1_eq α p.
We will prove PNo_rel_strict_upperbd L (ordsucc α) p1 ∧ PNo_rel_strict_lowerbd R (ordsucc α) p1.
Apply andI to the current goal.
We will prove PNo_rel_strict_upperbd L (ordsucc α) p1.
Let γ be given.
Assume Hc: γ ∈ ordsucc α.
Let q be given.
Assume Hq: PNo_downc L γ q.
We prove the intermediate claim Lc: ordinal γ.
An exact proof term for the current goal is ordinal_Hered (ordsucc α) Lsa γ Hc.
We will prove PNoLt γ q (ordsucc α) p1.
Apply PNoLt_tra γ α (ordsucc α) Lc Ha Lsa q p p1 to the current goal.
We will prove PNoLt γ q α p.
Apply Hq to the current goal.
Let δ be given.
Assume Hq1.
Apply Hq1 to the current goal.
Assume Hd: ordinal δ.
Assume Hq1.
Apply Hq1 to the current goal.
Let r be given.
Assume Hq1.
Apply Hq1 to the current goal.
Assume Hr: L δ r.
Assume Hqr: PNoLe γ q δ r.
We prove the intermediate claim Ldr: PNo_downc L δ r.
We will prove ∃β, ordinal β ∧ ∃q : set → prop, L β q ∧ PNoLe δ r β q.
We use δ 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 γ δ α Lc Hd Ha q r p Hqr to the current goal.
We will prove PNoLt δ r α p.
An exact proof term for the current goal is Hp1a δ (HaL δ r Hr) r Ldr.
We will prove PNoLt α p (ordsucc α) p1.
Apply PNoLtI2 to the current goal.
We will prove α ∈ ordsucc α.
Apply ordsuccI2 to the current goal.
We will prove PNoEq_ α p p1.
An exact proof term for the current goal is Lpp1e.
We will prove p1 α.
We will prove p α ∨ α = α.
Apply orIR to the current goal.
Use reflexivity.
We will prove PNo_rel_strict_lowerbd R (ordsucc α) p1.
Let γ be given.
Assume Hc: γ ∈ ordsucc α.
Let q be given.
Assume Hq: PNo_upc R γ q.
We prove the intermediate claim Lc: ordinal γ.
An exact proof term for the current goal is ordinal_Hered (ordsucc α) Lsa γ Hc.
We will prove PNoLt (ordsucc α) p1 γ q.
Apply Hq to the current goal.
Let δ be given.
Assume Hq1.
Apply Hq1 to the current goal.
Assume Hd: ordinal δ.
Assume Hq1.
Apply Hq1 to the current goal.
Let r be given.
Assume Hq1.
Apply Hq1 to the current goal.
Assume Hr: R δ r.
Assume Hrq: PNoLe δ r γ q.
Apply (λH : PNoLt (ordsucc α) p1 δ r ⇒ PNoLtLe_tra (ordsucc α) δ γ Lsa Hd Lc p1 r q H Hrq) to the current goal.
We will prove PNoLt (ordsucc α) p1 δ r.
We prove the intermediate claim Lda: δ ∈ α.
An exact proof term for the current goal is HaR δ r Hr.
We prove the intermediate claim Ldsa: δ ∈ ordsucc α.
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 δ r.
We will prove ∃β, ordinal β ∧ ∃q : set → prop, R β q ∧ PNoLe β q δ r.
We use δ 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 α p δ r.
An exact proof term for the current goal is Hp1b δ Lda r Ldr.
Apply PNoLt_trichotomy_or δ (ordsucc α) r p1 Hd Lsa to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: PNoLt δ r (ordsucc α) p1.
We will prove False.
Apply PNoLt_irref α p to the current goal.
We will prove PNoLt α p α p.
Apply PNoLt_tra α δ α Ha Hd Ha p r p Lpr to the current goal.
We will prove PNoLt δ r α p.
Apply PNoLtE δ (ordsucc α) r p1 H1 to the current goal.
Assume H2: PNoLt_ (δ ∩ ordsucc α) r p1.
Apply H2 to the current goal.
Let eps be given.
Assume H3.
Apply H3 to the current goal.
Assume He: eps ∈ δ ∩ ordsucc α.
Apply binintersectE δ (ordsucc α) eps He to the current goal.
Assume He1 He2.
We prove the intermediate claim Lea: eps ∈ α.
An exact proof term for the current goal is Ha1 δ 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_ (δ ∩ α) r p.
We will prove ∃β ∈ δ ∩ α, PNoEq_ β r p ∧ ¬ r β ∧ p β.
We use eps to witness the existential quantifier.
Apply andI to the current goal.
We will prove eps ∈ δ ∩ α.
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 α 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 = α.
We will prove False.
Apply In_irref α 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: δ ∈ ordsucc α.
Assume H3: PNoEq_ δ r p1.
Assume H4: p1 δ.
Apply PNoLtI2 δ α r p Lda to the current goal.
We will prove PNoEq_ δ r p.
Apply PNoEq_tra_ δ r p1 p to the current goal.
An exact proof term for the current goal is H3.
Apply PNoEq_antimon_ p1 p α Ha δ 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 δ.
Apply H4 to the current goal.
An exact proof term for the current goal is (λH ⇒ H).
Assume H5: δ = α.
We will prove False.
Apply In_irref α 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 α ∈ δ.
We will prove False.
An exact proof term for the current goal is In_no2cycle δ (ordsucc α) Ldsa H2.
Assume H1.
Apply H1 to the current goal.
Assume H2: δ = ordsucc α.
We will prove False.
Apply In_irref δ 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.
∎