--

theorem ex : Not (1 = 2) :=
of_decide_eq_false rfl