Let R 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.
Let γ be given.
Assume Hc.
Let q be given.
Assume H4.
We will
prove PNoLt β p γ q.
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 α p γ q.
Apply H1 to the current goal.
An exact proof term for the current goal is Lca.
An exact proof term for the current goal is H4.
Apply PNoLtE α γ p q L1 to the current goal.
We prove the intermediate
claim L2:
α ∩ γ = γ.
An exact proof term for the current goal is Ha1 γ Lca.
We prove the intermediate
claim L3:
β ∩ γ = γ.
An exact proof term for the current goal is Lbt γ Hc.
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.
An
exact proof term for the current goal is
In_no2cycle α γ H5 Lca.
An exact proof term for the current goal is Hc.
An exact proof term for the current goal is H6.
An exact proof term for the current goal is H7.
∎