fact: Fixpoint fv_tt (T : typ) {struct T} : atoms := match T with | typ_top => {} | typ_bvar J => {} | typ_fvar X => {{ X }} | typ_arrow T1 T2 => (fv_tt T1) `union` (fv_tt T2) | typ_all T1 T2 => (fv_tt T1) `union` (fv_tt T2) | typ_sum T1 T2 => (fv_tt T1) `union` (fv_tt T2) end.
imports: Fsub.Fsub_LetSum_Definitions