Let α be given.
Assume H1: TransSet α ∧ ∀β ∈ α, TransSet β.
Apply H1 to the current goal.
Assume H2: TransSet α.
Assume H3: ∀β ∈ α, TransSet β.
We will prove TransSet (ordsucc α) ∧ ∀β ∈ ordsucc α, TransSet β.
Apply andI to the current goal.
An exact proof term for the current goal is (TransSet_ordsucc α H2).
Let β be given.
Assume H4: β ∈ ordsucc α.
We will prove TransSet β.
Apply (ordsuccE α β H4) to the current goal.
Assume H5: β ∈ α.
An exact proof term for the current goal is (H3 β H5).
Assume H5: β = α.
rewrite the current goal using H5 (from left to right).
An exact proof term for the current goal is H2.
∎