Let a and b be given.

Assume Ha Hb Hab.

We will prove a ∈ R ∧ b ∈ R ∧ a < b.

Apply and3I to the current goal.

An exact proof term for the current goal is Ha.

An exact proof term for the current goal is Hb.

An exact proof term for the current goal is Hab.

∎