proposition: Lemma subst_ee_expr : forall z e1 e2, expr e1 -> expr e2 -> expr (subst_ee z e2 e1).
proof: Proof. Proof with auto. intros z e1 e2 He1 He2. induction He1; simpl; auto; try solve [ econstructor; try instantiate (1 := L `union` singleton z); intros; try rewrite subst_ee_open_ee_var; try rewrite subst_ee_open_te_var; instantiate; auto ]. Case "expr_var". destruct (x == z)... Qed.
imports: Fsub.Fsub_LetSum_Definitions