proposition: Lemma subst_tt_intro : forall X T2 U, X `notin` fv_tt T2 -> open_tt T2 U = subst_tt X U (open_tt T2 X).
proof: Proof. Proof with auto. intros. unfold open_tt. apply subst_tt_intro_rec... Qed.
imports: Fsub.Fsub_LetSum_Definitions