let d_disj = function Disj(dl) -> dl | _ -> invalid_arg "wrong propositional argument"