+(* NOTATION
+Notation "{ x : A | P }" := (sigT (fun x : A => P):CProp)
+ (at level 0, x at level 99) : type_scope.
+*)
+
+(* NOTATION
+Notation "{ x : A | P | Q }" :=
+ (sig2T A (fun x : A => P) (fun x : A => Q)) (at level 0, x at level 99) :
+ type_scope.
+*)
+