fact: Fixpoint subst_exp (u:exp) (y:var) (e:exp) {struct e} : exp := match e with | (var_b n) => var_b n | (var_f x) => (if x == y then u else (var_f x)) | (abs e1) => abs (subst_exp u y e1) | (app e1 e2) => app (subst_exp u y e1) (subst_exp u y e2) end.
imports: Metalib.Metatheory