fact: Fixpoint subst_ee (z : atom) (u : exp) (e : exp) {struct e} : exp := match e with | exp_bvar i => exp_bvar i | exp_fvar x => if x == z then u else e | exp_abs V e1 => exp_abs V (subst_ee z u e1) | exp_app e1 e2 => exp_app (subst_ee z u e1) (subst_ee z u e2) | exp_tabs V e1 => exp_tabs V (subst_ee z u e1) | exp_tapp e1 V => exp_tapp (subst_ee z u e1) V | exp_let e1 e2 => exp_let (subst_ee z u e1) (subst_ee z u e2) | exp_inl e1 => exp_inl (subst_ee z u e1) | exp_inr e1 => exp_inr (subst_ee z u e1) | exp_case e1 e2 e3 => exp_case (subst_ee z u e1) (subst_ee z u e2) (subst_ee z u e3) end.
imports: Fsub.Fsub_LetSum_Definitions