proposition: Lemma subst_ee_open_te_var : forall z (X:atom) u e, expr u -> open_te (subst_ee z u e) X = subst_ee z u (open_te e X).
proof: Proof. Proof with auto. intros z X u e H. rewrite subst_ee_open_te... Qed.
imports: Fsub.Fsub_LetSum_Definitions