axiom orIR: !P:prop.!Q:prop.Q -> P | Q claim !P:prop.!Q:prop.!R:prop.R -> P | Q | R