Let R and α be given.
Let β be given.
Let p be given.
Let γ be given.
Let q be given.
Apply Ha to the current goal.
Assume Ha1 _.
We prove the intermediate
claim Lb:
ordinal β.
We prove the intermediate
claim Lb1:
TransSet β.
Apply Lb to the current goal.
Assume H _.
An exact proof term for the current goal is H.
We prove the intermediate
claim Lc:
ordinal γ.
An
exact proof term for the current goal is
ordinal_Hered β Lb γ Hc.
We prove the intermediate
claim Lcb:
γ ⊆ β.
An exact proof term for the current goal is Lb1 γ Hc.
We will
prove PNoLt β p γ q.
Apply Hq to the current goal.
Let δ be given.
Assume H2.
Apply H2 to the current goal.
Assume H2.
Apply H2 to the current goal.
Let r be given.
Assume H2.
Apply H2 to the current goal.
Assume H2: R δ r.
We prove the intermediate
claim L1:
PNoLt α p δ r.
An exact proof term for the current goal is H1 δ Hd r H2.
We prove the intermediate
claim L2:
PNoLt α p γ q.
An
exact proof term for the current goal is
PNoLtLe_tra α δ γ Ha Hd Lc p r q L1 H3.
We prove the intermediate
claim Lca:
γ ∈ α.
Apply ordsuccE α β Hb to the current goal.
An exact proof term for the current goal is Ha1 β Hb1 γ Hc.
rewrite the current goal using Hb1 (from right to left).
An exact proof term for the current goal is Hc.
We prove the intermediate
claim Lca2:
γ ⊆ α.
An exact proof term for the current goal is Ha1 γ Lca.
We will
prove PNoLt β p γ q.
Assume H4.
Apply H4 to the current goal.
Apply PNoLtE γ β q p H4 to the current goal.
Apply H5 to the current goal.
Apply PNoLt_tra α γ α Ha Lc Ha p q p to the current goal.
We will
prove PNoLt α p γ q.
An exact proof term for the current goal is L2.
We will
prove PNoLt γ q α p.
An exact proof term for the current goal is H5.
Assume H7: p γ.
Apply PNoLt_tra α γ α Ha Lc Ha p q p to the current goal.
We will
prove PNoLt α p γ q.
An exact proof term for the current goal is L2.
We will
prove PNoLt γ q α p.
An exact proof term for the current goal is Lca.
An exact proof term for the current goal is H6.
We will prove p γ.
An exact proof term for the current goal is H7.
An
exact proof term for the current goal is
In_no2cycle β γ H5 Hc.
Assume H4.
Apply H4 to the current goal.
rewrite the current goal using H4 (from right to left) at position 1.
An exact proof term for the current goal is Hc.
Assume H4.
An exact proof term for the current goal is H4.
∎