
(* For extracting a decision procedure which returns either a 
   derivation or a countermodel, activate the following: *)

(* Require Export Derivable_Def_compute_derivations. *)

(* OR *)

(* For extracting a decision procedure which returns either 
   "derivable" or a countermodel, activate the following: *)

Require Export Derivable_Def_dont_compute_derivations.