theory False
imports Main
begin

lemma f: False proof -
  {
    fix A B :: bool and f
    assume A: "A=B"
    have "f(A)" by (simp add: A A[symmetric])
  } note this[of True True Not]
  thus False by simp
qed

lemma "(1::nat) = 2" using f by simp

end