(**************************************************************************)
(*  Si tenemos un predicado P  decidible sobre X:Set, entonces            *)
(*  podemos definir la funcion caracteristica que vale "true" en los x:X  *)
(*  donde se cumple P (o sea aquellos x para los que (P x) es cierto)  y  *)
(*  "false" en los que no.                                                *)
(**************************************************************************)



Section discriminante.
Definition ifdec:=[A,B:Prop; C:Set; H:({A}+{B}); x,y:C]
 Cases H of
   (left _) => x
 | (right _) => y
 end.
Variable X:Set.
Variable P:X->Prop.
Variable H:(x:X){(P x)}+{~(P x)}.

Definition  disc:=[x:X](ifdec (P x) ~(P x) bool (H x) true false).

End discriminante.
(* Check disc.
disc
     : (X:Set; P:(X->Prop))((x:X){(P x)}+{~(P x)})->X->bool
*)

(* Probar:
Lemma uno:(x:X)(P x)<->(disc x)=true.

Lemma dos: (x:X)~(P x) <-> (disc x)=false.
*)