fact: Fixpoint subst_tt (Z : atom) (U : typ) (T : typ) {struct T} : typ := match T with | typ_top => typ_top | typ_bvar J => typ_bvar J | typ_fvar X => if X == Z then U else T | typ_arrow T1 T2 => typ_arrow (subst_tt Z U T1) (subst_tt Z U T2) | typ_all T1 T2 => typ_all (subst_tt Z U T1) (subst_tt Z U T2) | typ_sum T1 T2 => typ_sum (subst_tt Z U T1) (subst_tt Z U T2) end.
imports: Fsub.Fsub_LetSum_Definitions