proposition: Lemma open_ee_body_e : forall e1 e2, body_e e1 -> expr e2 -> expr (open_ee e1 e2).
proof: Proof. intros e1 e2 [L H] J. pick fresh x. rewrite (subst_ee_intro x); auto using subst_ee_expr. Qed.
imports: Fsub.Fsub_LetSum_Definitions