module ProverWhy3:sig
..end
val add_specific_equality : for_tau:(Lang.tau -> bool) -> mk_new_eq:Lang.F.binop -> unit
Equality used in the goal, simpler to prove than polymorphic equality
val prove : ?mode:VCS.mode ->
?timeout:int ->
?steplimit:int -> prover:Why3Provers.t -> Wpo.t -> VCS.result Task.task
Return NoResult if it is already proved by Qed