intros. elim H. assumption.
qed.
inductive Or (A,B:Prop) : Prop \def
or_introl : A \to (Or A B)
| or_intror : B \to (Or A B).
intros. elim H. assumption.
qed.
inductive Or (A,B:Prop) : Prop \def
or_introl : A \to (Or A B)
| or_intror : B \to (Or A B).