Let L and α be given.
Assume Ha.
Let p and β be given.
Assume Hb.
Apply Ha to the current goal.
Assume Ha1 _.
We prove the intermediate claim Lb: ordinal β.
An exact proof term for the current goal is ordinal_Hered α Ha β Hb.
We prove the intermediate claim Lbt: TransSet β.
Apply Lb to the current goal.
Assume H2 _.
An exact proof term for the current goal is H2.
Assume H1: ∀γ ∈ α, ∀q : set → prop, PNo_downc L γ q → PNoLt γ q α p.
We will prove ∀γ ∈ β, ∀q : set → prop, PNo_downc L γ q → PNoLt γ q β p.
Let γ be given.
Assume Hc.
Let q be given.
Assume H4.
We will prove PNoLt γ q β p.
We prove the intermediate claim Lca: γ ∈ α.
An exact proof term for the current goal is Ha1 β Hb γ Hc.
We prove the intermediate claim L1: PNoLt γ q α p.
Apply H1 to the current goal.
We will prove γ ∈ α.
An exact proof term for the current goal is Lca.
We will prove PNo_downc L γ q.
An exact proof term for the current goal is H4.
Apply PNoLtE γ α q p L1 to the current goal.
Assume H5: PNoLt_ (γ ∩ α) q p.
We prove the intermediate claim L2: γ ∩ α = γ.
Apply binintersect_Subq_eq_1 to the current goal.
An exact proof term for the current goal is Ha1 γ Lca.
We prove the intermediate claim L3: γ ∩ β = γ.
Apply binintersect_Subq_eq_1 to the current goal.
An exact proof term for the current goal is Lbt γ Hc.
Apply PNoLtI1 to the current goal.
rewrite the current goal using L3 (from left to right).
rewrite the current goal using L2 (from right to left).
An exact proof term for the current goal is H5.
Assume H5: γ ∈ α.
Assume H6: PNoEq_ γ q p.
Assume H7: p γ.
Apply PNoLtI2 to the current goal.
We will prove γ ∈ β.
An exact proof term for the current goal is Hc.
We will prove PNoEq_ γ q p.
An exact proof term for the current goal is H6.
We will prove p γ.
An exact proof term for the current goal is H7.
Assume H5: α ∈ γ.
We will prove False.
An exact proof term for the current goal is In_no2cycle α γ H5 Lca.
∎