fact: Fixpoint open_exp_wrt_exp_rec (k:nat) (u:exp) (e:exp) {struct e}: exp := match e with | (var_b n) => match lt_eq_lt_dec n k with | inleft (left _) => var_b n | inleft (right _) => u | inright _ => var_b (n - 1) end | (var_f x) => var_f x | (abs e) => abs (open_exp_wrt_exp_rec (S k) u e) | (app e1 e2) => app (open_exp_wrt_exp_rec k u e1) (open_exp_wrt_exp_rec k u e2) end.
imports: Metalib.Metatheory