simp_rw [hf] at heq
case h
heq : (fun x => 0) '' {a | a = 1 ∧ a = 2} = {0}
hf : ∀ {a : ℤ}, (a = 1 ∧ a = 2) = False
⊢ False
case h
hf : ∀ {a : ℤ}, (a = 1 ∧ a = 2) = False
heq : (fun x => 0) '' {a | False} = {0}
⊢ False