proposition: Lemma subst_ee_open_te : forall e P z u, expr u -> subst_ee z u (open_te e P) = open_te (subst_ee z u e) P.
proof: Proof. Proof with auto. intros. unfold open_te. apply subst_ee_open_te_rec... Qed.
imports: Fsub.Fsub_LetSum_Definitions