interpretation "logical or" 'or x y = (Or x y).
-(* BUG HERE: WHY IS IT ACCEPTED??? *)
-inductive Ex (A:Type[1]) (P:A \to CProp[1]) : CProp[0] \def
- ex_intro: \forall x:A. P x \to Ex A P.
+ninductive Ex (A:Type) (P:A → CProp) : CProp ≝
+ ex_intro: ∀x:A. P x → Ex A P.
interpretation "exists" 'exists x = (Ex ? x).
\ No newline at end of file