theory Inconsistency
imports Main
begin

(* a legal definition *)
constdefs
  consA :: "'a * bool"
  "consA == (arbitrary::'a, ALL (x::'a) (y::'a). x = y)"

consts
  consB :: bool

(* not a legal definition *)
axioms
  consB_def: "consB == snd consA"

lemma "True = False"
proof -
  have "True = (ALL (x::unit) y. x = y)" by simp
  also have "\<dots> = consB"
    by (simp add: consA_def consB_def [where 'a=unit])
  also have "\<dots> = (ALL (x::bool) y. x = y)"
    by (simp add: consA_def consB_def [where 'a=bool])
  also have "\<dots> = False" by auto
  finally show ?thesis .
qed

end