let mk_disj = function
  | [] -> False
  | pl -> Disj(pl)