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