equal
deleted
inserted
replaced
374 proof - |
374 proof - |
375 have "atom x \<sharp> Lam [x]. Var x" by (simp add: lam.fresh) |
375 have "atom x \<sharp> Lam [x]. Var x" by (simp add: lam.fresh) |
376 moreover |
376 moreover |
377 have "Lam [x]. Var x \<mapsto> Var x" using unbind_simple by auto |
377 have "Lam [x]. Var x \<mapsto> Var x" using unbind_simple by auto |
378 ultimately |
378 ultimately |
379 have "atom x \<sharp> Var x" using unbind_fake by auto |
379 have "atom x \<sharp> Var x" using unbind_fake by blast |
380 then have "x \<noteq> x" by (simp add: lam.fresh fresh_at_base) |
380 then have "x \<noteq> x" by (simp add: lam.fresh fresh_at_base) |
381 then show "False" by simp |
381 then show "False" by simp |
382 qed |
382 qed |
383 |
383 |
384 end |
384 end |