proposition: Lemma subst_tt_open_tt : forall T1 T2 (X:atom) P, type P -> subst_tt X P (open_tt T1 T2) = open_tt (subst_tt X P T1) (subst_tt X P T2).
proof: Proof. Proof with auto. intros. unfold open_tt. apply subst_tt_open_tt_rec... Qed.
imports: Fsub.Fsub_LetSum_Definitions