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