val absurd : unit -> unit
val contradiction : unit -> unit
val decompose : unit -> unit
+ val injection : unit -> unit
+ val discriminate : unit -> unit
val whd_in_scratch : unit -> unit
val reduce_in_scratch : unit -> unit
val simpl_in_scratch : unit -> unit