An exact proof term for the current goal is (SepE1 rational_numbers (λq0 : set ⇒ mul_SNo q0 q0 < 2) q Hq).