INDUCTIVE DEFINITION or () [ :Prop, :Prop ]
OF ARITY Prop
BUILT FROM:
     or_introl: A→(or A B)
   | or_intror: B→(or A B)