interpretation "logical or" 'or x y =
(cic:/matita/logic/connectives/Or.ind#xpointer(1/1) x y).
-definition decidable : Prop \to Prop \def \lambda A:Prop. A \lor \not A.
+definition decidable : Prop \to Prop \def \lambda A:Prop. A \lor \lnot A.
inductive ex (A:Type) (P:A \to Prop) : Prop \def
ex_intro: \forall x:A. P x \to ex A P.