have hf {a : ℤ} : (a = 1 ∧ a = 2) = False := by
  simp_all only [eq_iff_iff, iff_false, not_and, OfNat.one_ne_ofNat, not_false_eq_true, implies_true]
case h
heq : (fun x => 0) '' {a | a = 1 ∧ a = 2} = {0}
⊢ False
case h
heq : (fun x => 0) '' {a | a = 1 ∧ a = 2} = {0}
hf : ∀ {a : ℤ}, (a = 1 ∧ a = 2) = False
⊢ False