fact: Fixpoint open_ee_rec (k : nat) (f : exp) (e : exp) {struct e} : exp := match e with | exp_bvar i => if k == i then f else (exp_bvar i) | exp_fvar x => exp_fvar x | exp_abs V e1 => exp_abs V (open_ee_rec (S k) f e1) | exp_app e1 e2 => exp_app (open_ee_rec k f e1) (open_ee_rec k f e2) | exp_tabs V e1 => exp_tabs V (open_ee_rec k f e1) | exp_tapp e1 V => exp_tapp (open_ee_rec k f e1) V | exp_let e1 e2 => exp_let (open_ee_rec k f e1) (open_ee_rec (S k) f e2) | exp_inl e1 => exp_inl (open_ee_rec k f e1) | exp_inr e2 => exp_inr (open_ee_rec k f e2) | exp_case e1 e2 e3 => exp_case (open_ee_rec k f e1) (open_ee_rec (S k) f e2) (open_ee_rec (S k) f e3) end.
imports: Metalib.Metatheory String