equal
deleted
inserted
replaced
519 show "alpha_lam_raw (subst_raw a y c) (subst_raw b y d)" |
519 show "alpha_lam_raw (subst_raw a y c) (subst_raw b y d)" |
520 using c d equivp_transp[OF lam_equivp] by blast |
520 using c d equivp_transp[OF lam_equivp] by blast |
521 qed |
521 qed |
522 |
522 |
523 lemma simp3: |
523 lemma simp3: |
524 "x \<noteq> y \<Longrightarrow> atom x \<notin> fv_lam_raw s \<Longrightarrow> Lam_raw x (subst_raw t y s) = Lam_raw x (subst_raw t y s)" |
524 "x \<noteq> y \<Longrightarrow> atom x \<notin> fv_lam_raw s \<Longrightarrow> subst_raw (Lam_raw x t) y s = Lam_raw x (subst_raw t y s)" |
525 by simp |
525 by simp |
526 |
526 |
527 lemmas subst_simps = subst_raw.simps(1-2)[quot_lifted,no_vars] |
527 lemmas subst_simps = subst_raw.simps(1-2)[quot_lifted,no_vars] |
528 simp3[quot_lifted,simplified lam.supp,simplified fresh_def[symmetric], no_vars] |
528 simp3[quot_lifted,simplified lam.supp,simplified fresh_def[symmetric], no_vars] |
529 |
529 |