fact: Fixpoint is_free (n : name) (t : type) := match t with | Tvar k => if k =? n then true else false | Arrow t1 t2 => (is_free n t1) || (is_free n t2) | Forall k t1 => if n =? k then false else (is_free n t1) end.
imports: List Arith Bool