proposition: Lemma subst_te_intro : forall X e U, X `notin` fv_te e -> open_te e U = subst_te X U (open_te e X).
proof: Proof. Proof with auto. intros. unfold open_te. apply subst_te_intro_rec... Qed.
imports: Fsub.Fsub_LetSum_Definitions