let rec libre x = function 
    Tint -> false
  | Tvar n -> x = n
  | Tarrow (t1, t2) -> libre x t1 || libre x t2;;