fact: Fixpoint subst (z : atom) (u : exp) (e : exp) {struct e} : exp := match e with | bvar i => bvar i | fvar x => if x == z then u else (fvar x) | abs t e1 => abs t (subst z u e1) | app e1 e2 => app (subst z u e1) (subst z u e2) end.
imports: Metalib.Metatheory