proposition: Lemma subst_te_open_ee_var : forall Z (x:atom) P e, open_ee (subst_te Z P e) x = subst_te Z P (open_ee e x).
proof: Proof. Proof with auto. intros. rewrite subst_te_open_ee... Qed.
imports: Fsub.Fsub_LetSum_Definitions