or_introl : A \to (Or A B)
| or_intror : B \to (Or A B).
-(*CSC: the URI must disappear: there is a bug now *)
interpretation "logical or" 'or x y = (Or x y).
theorem Or_ind':
inductive ex (A:Type) (P:A \to Prop) : Prop \def
ex_intro: \forall x:A. P x \to ex A P.
-interpretation "exists" 'exists \eta.x = (ex _ x).
+interpretation "exists" 'exists x = (ex _ x).
inductive ex2 (A:Type) (P,Q:A \to Prop) : Prop \def
ex_intro2: \forall x:A. P x \to Q x \to ex2 A P Q.