proposition: Lemma subst_ee_intro : forall x e u, x `notin` fv_ee e -> open_ee e u = subst_ee x u (open_ee e x).
proof: Proof. Proof with auto. intros. unfold open_ee. apply subst_ee_intro_rec... Qed.
imports: Fsub.Fsub_LetSum_Definitions