Let L and alpha be given.

Assume Ha.

Let p and beta be given.

Assume Hb.

Apply Ha to the current goal.

Assume Ha1 _.

We prove the intermediate claim Lb: ordinal beta.

An exact proof term for the current goal is ordinal_Hered alpha Ha beta Hb.

We prove the intermediate claim Lbt: TransSet beta.

Apply Lb to the current goal.

Assume H2 _.

An exact proof term for the current goal is H2.

Assume H1: ∀gamma ∈ alpha, ∀q : set → prop, PNo_downc L gamma q → PNoLt gamma q alpha p.

We will prove ∀gamma ∈ beta, ∀q : set → prop, PNo_downc L gamma q → PNoLt gamma q beta p.

Let gamma be given.

Assume Hc.

Let q be given.

Assume H4.

We will prove PNoLt gamma q beta p.

We prove the intermediate claim Lca: gamma ∈ alpha.

An exact proof term for the current goal is Ha1 beta Hb gamma Hc.

We prove the intermediate claim L1: PNoLt gamma q alpha p.

Apply H1 to the current goal.

We will prove gamma ∈ alpha.

An exact proof term for the current goal is Lca.

We will prove PNo_downc L gamma q.

An exact proof term for the current goal is H4.

Apply PNoLtE gamma alpha q p L1 to the current goal.

Assume H5: PNoLt_ (gamma ∩ alpha) q p.

We prove the intermediate claim L2: gamma ∩ alpha = gamma.

Apply binintersect_Subq_eq_1 to the current goal.

An exact proof term for the current goal is Ha1 gamma Lca.

We prove the intermediate claim L3: gamma ∩ beta = gamma.

Apply binintersect_Subq_eq_1 to the current goal.

An exact proof term for the current goal is Lbt gamma 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: gamma ∈ alpha.

Assume H6: PNoEq_ gamma q p.

Assume H7: p gamma.

Apply PNoLtI2 to the current goal.

We will prove gamma ∈ beta.

An exact proof term for the current goal is Hc.

We will prove PNoEq_ gamma q p.

An exact proof term for the current goal is H6.

We will prove p gamma.

An exact proof term for the current goal is H7.

Assume H5: alpha ∈ gamma.

We will prove False.

An exact proof term for the current goal is In_no2cycle alpha gamma H5 Lca.

∎