TODO
----

- axiomes pour les prédicats récursifs comme

  Fixpoint even (n:nat) : Prop :=
  match n with 
  O => True
  | S O => False
  | S (S p) => even p
  end.

  ou encore In sur les listes du module Coq List.

- discriminate

- inversion (Set et Prop)


BUGS
----