proposition: Lemma notin_fv_tt_open : forall (Y X : atom) T, X `notin` fv_tt (open_tt T Y) -> X `notin` fv_tt T.
proof: Proof. intros Y X T. unfold open_tt. generalize 0. induction T; simpl; intros k Fr; eauto. Qed.
imports: Fsub.Fsub_LetSum_Infrastructure