Let L and R be given.
Assume HLR.
Let α be given.
Assume Ha.
Let p and q be given.
Assume Hp.
Assume Hq.
Apply Ha to the current goal.
Assume Ha1 _.
Apply Hp to the current goal.
Assume Hp1.
Apply Hp1 to the current goal.
Assume _.
Assume Hp1: PNo_strict_imv L R α p.
Assume Hp2: ∀β ∈ α, ∀r : set → prop, ¬ PNo_strict_imv L R β r.
Apply Hp1 to the current goal.
Assume Hp1a: PNo_strict_upperbd L α p.
Assume Hp1b: PNo_strict_lowerbd R α p.
Apply Hq to the current goal.
Assume Hq1: PNo_strict_upperbd L α q.
Assume Hq2: PNo_strict_lowerbd R α q.
We prove the intermediate claim L1: ∀β, ordinal β → β ∈ α → (p β ↔ q β).
Apply ordinal_ind to the current goal.
Let β be given.
Assume Hb1: ordinal β.
Assume IH: ∀γ ∈ β, γ ∈ α → (p γ ↔ q γ).
Assume Hb2: β ∈ α.
We prove the intermediate claim Lbpq: PNoEq_ β p q.
Let γ be given.
Assume Hc: γ ∈ β.
An exact proof term for the current goal is IH γ Hc (Ha1 β Hb2 γ Hc).
We will prove p β ↔ q β.
Apply iffI to the current goal.
Assume H1: p β.
We will prove q β.
Apply dneg to the current goal.
Assume H2: ¬ q β.
We prove the intermediate claim Lqp: PNoLt β q α p.
Apply PNoLtI2 to the current goal.
We will prove β ∈ α.
An exact proof term for the current goal is Hb2.
We will prove PNoEq_ β q p.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is Lbpq.
We will prove p β.
An exact proof term for the current goal is H1.
We prove the intermediate claim Lqq: PNoLt α q β q.
Apply PNoLtI3 to the current goal.
We will prove β ∈ α.
An exact proof term for the current goal is Hb2.
We will prove PNoEq_ β q q.
Apply PNoEq_ref_ to the current goal.
We will prove ¬ q β.
An exact proof term for the current goal is H2.
Apply Hp2 β Hb2 q to the current goal.
We will prove PNo_strict_imv L R β q.
We will prove PNo_strict_upperbd L β q ∧ PNo_strict_lowerbd R β q.
Apply andI to the current goal.
Let γ be given.
Assume Hc: ordinal γ.
Let r be given.
Assume Hr: L γ r.
We will prove PNoLt γ r β q.
Apply PNoLt_tra γ α β Hc Ha Hb1 r q q to the current goal.
We will prove PNoLt γ r α q.
An exact proof term for the current goal is Hq1 γ Hc r Hr.
We will prove PNoLt α q β q.
An exact proof term for the current goal is Lqq.
Let γ be given.
Assume Hc: ordinal γ.
Let r be given.
Assume Hr: R γ r.
We will prove PNoLt β q γ r.
Apply PNoLt_tra β α γ Hb1 Ha Hc q p r to the current goal.
We will prove PNoLt β q α p.
An exact proof term for the current goal is Lqp.
We will prove PNoLt α p γ r.
An exact proof term for the current goal is Hp1b γ Hc r Hr.
Assume H1: q β.
We will prove p β.
Apply dneg to the current goal.
Assume H2: ¬ p β.
We prove the intermediate claim Lpq: PNoLt α p β q.
Apply PNoLtI3 to the current goal.
We will prove β ∈ α.
An exact proof term for the current goal is Hb2.
We will prove PNoEq_ β p q.
An exact proof term for the current goal is Lbpq.
We will prove ¬ p β.
An exact proof term for the current goal is H2.
We prove the intermediate claim Lqq: PNoLt β q α q.
Apply PNoLtI2 to the current goal.
We will prove β ∈ α.
An exact proof term for the current goal is Hb2.
We will prove PNoEq_ β q q.
Apply PNoEq_ref_ to the current goal.
We will prove q β.
An exact proof term for the current goal is H1.
Apply Hp2 β Hb2 q to the current goal.
We will prove PNo_strict_imv L R β q.
We will prove PNo_strict_upperbd L β q ∧ PNo_strict_lowerbd R β q.
Apply andI to the current goal.
Let γ be given.
Assume Hc: ordinal γ.
Let r be given.
Assume Hr: L γ r.
We will prove PNoLt γ r β q.
Apply PNoLt_tra γ α β Hc Ha Hb1 r p q to the current goal.
We will prove PNoLt γ r α p.
An exact proof term for the current goal is Hp1a γ Hc r Hr.
We will prove PNoLt α p β q.
An exact proof term for the current goal is Lpq.
Let γ be given.
Assume Hc: ordinal γ.
Let r be given.
Assume Hr: R γ r.
We will prove PNoLt β q γ r.
Apply PNoLt_tra β α γ Hb1 Ha Hc q q r to the current goal.
We will prove PNoLt β q α q.
An exact proof term for the current goal is Lqq.
We will prove PNoLt α q γ r.
An exact proof term for the current goal is Hq2 γ Hc r Hr.
Let β be given.
Assume Hb: β ∈ α.
An exact proof term for the current goal is L1 β (ordinal_Hered α Ha β Hb) Hb.
∎