let d_iff = function Iff(p, q) -> (p, q) | _ -> invalid_arg "wrong propositional argument"