476 

   477 fun

   478   subst_var_raw :: "lam_raw \<Rightarrow> name \<Rightarrow> name \<Rightarrow> lam_raw"

   479 where

   480   "subst_var_raw (Var_raw x) y s = (if x=y then (Var_raw s) else (Var_raw x))"

   481 | "subst_var_raw (App_raw l r) y s = App_raw (subst_var_raw l y s) (subst_var_raw r y s)"

   482 | "subst_var_raw (Lam_raw x t) y s =

   483      (if x = y then Lam_raw x t else Lam_raw x (subst_var_raw t y s))"

   484 

   485 (* Should be true? *)

   486 lemma "(alpha_lam_raw ===> op = ===> op = ===> alpha_lam_raw) subst_var_raw subst_var_raw"

   487   proof (intro fun_relI, (simp, clarify))

   488     fix a b ba bb

   489     assume a: "alpha_lam_raw a b"

   490     show "alpha_lam_raw (subst_var_raw a ba bb) (subst_var_raw b ba bb)" using a

   491       apply (induct a b rule: alpha_lam_raw.induct)

   492       apply (simp add: equivp_reflp[OF lam_equivp])

   493       apply (simp add: alpha_lam_raw.intros)

   494       apply auto

   495       apply (rule_tac[!] alpha_lam_raw.intros)

   496       apply (rule_tac[!] x="p" in exI) (* Need to do better *)

   497       apply (simp_all add: alphas)

   498       apply clarify

   499       apply simp

   500       sorry

   501     qed

   502