Let n be given.
Assume Hn.
Let x be given.
An exact proof term for the current goal is Hx1a.
We prove the intermediate
claim L2:
x = 0.
An
exact proof term for the current goal is
SNoLev_0_eq_0 x Hx1c H1.
rewrite the current goal using L2 (from left to right) at position 1.
An exact proof term for the current goal is Hx2.
Assume H1.
Apply H1 to the current goal.
Let m be given.
Assume H1.
Apply H1 to the current goal.
We use m to witness the existential quantifier.
Apply andI to the current goal.
rewrite the current goal using Hm2 (from left to right).
We will
prove x = eps_ m.
An exact proof term for the current goal is Hm2.
An exact proof term for the current goal is Hx3.
rewrite the current goal using Hm2 (from left to right).
Let k be given.
We prove the intermediate
claim L3:
ordinal k.
Apply iffI to the current goal.
Apply SingI to the current goal.
Apply SingI to the current goal.
∎