Let x and y be given.

Assume Hx Hy.

Let p be given.

Assume Hp1 Hp2 Hp3 Hp4 Hp5 Hp6 Hp7.

Apply SNoLt_trichotomy_or_impred x y Hx Hy to the current goal.

Assume H1: x < y.

Apply SNoLt_SNoL_or_SNoR_impred x y Hx Hy H1 to the current goal.

An exact proof term for the current goal is Hp2.

An exact proof term for the current goal is Hp3.

An exact proof term for the current goal is Hp4.

Assume H1: x = y.

An exact proof term for the current goal is Hp1 H1.

Assume H1: y < x.

Apply SNoLt_SNoL_or_SNoR_impred y x Hy Hx H1 to the current goal.

Let z be given.

Assume H2 H3.

An exact proof term for the current goal is Hp5 z H3 H2.

An exact proof term for the current goal is Hp7.

An exact proof term for the current goal is Hp6.

∎