proposition: Lemma subst_te_open_te : forall e T X U, type U -> subst_te X U (open_te e T) = open_te (subst_te X U e) (subst_tt X U T).
proof: Proof. Proof with auto. intros. unfold open_te. apply subst_te_open_te_rec... Qed.
imports: Fsub.Fsub_LetSum_Definitions