let rec occurs x = function
  | True -> false
  | False -> false
  | Var(y) -> Name.eq x y
  | Atom _ -> false
  | Disj(pl) -> List.exists (occurs x) pl
  | Iff(p, q) -> occurs x p || occurs x q
  | Neg(p) -> occurs x p
  | Let(y, p, q) -> if Name.eq x y then false else occurs x p || occurs x q
  | Ite(p, q, r) -> occurs x p || occurs x q || occurs x r