constant P : Prop constant Q : Prop axiom p_or_q : P + Q check p_or_q