equal
deleted
inserted
replaced
344 proof - |
344 proof - |
345 have "atom x \<sharp> Lam [x]. Var x" by (simp add: lam.fresh) |
345 have "atom x \<sharp> Lam [x]. Var x" by (simp add: lam.fresh) |
346 moreover |
346 moreover |
347 have "Lam [x]. Var x \<mapsto> Var x" using unbind_simple by auto |
347 have "Lam [x]. Var x \<mapsto> Var x" using unbind_simple by auto |
348 ultimately |
348 ultimately |
349 have "atom x \<sharp> Var x" using unbind_fake by auto |
349 have "atom x \<sharp> Var x" |
|
350 by (rule_tac unbind_fake) (auto) |
350 then have "x \<noteq> x" by (simp add: lam.fresh fresh_at_base) |
351 then have "x \<noteq> x" by (simp add: lam.fresh fresh_at_base) |
351 then show "False" by simp |
352 then show "False" by simp |
352 qed |
353 qed |
353 |
354 |
354 end |
355 end |