Let a be given.

Assume Ha.

Assume Haa.

We prove the intermediate claim Hlt: a < a.

An exact proof term for the current goal is (RltE_lt a a Haa).

An exact proof term for the current goal is ((SNoLt_irref a) Hlt).

∎