proposition: Lemma subst_te_open_ee : forall e1 e2 Z P, subst_te Z P (open_ee e1 e2) = open_ee (subst_te Z P e1) (subst_te Z P e2).
proof: Proof. Proof with auto. intros. unfold open_ee. apply subst_te_open_ee_rec... Qed.
imports: Fsub.Fsub_LetSum_Definitions