SEARCH MODULE Defines the proof search algorithm YOU HAVE TO WRITE THE PROVER WHICH GENERATES PROOF TERMS AS CERTIFICATES (see validation/proof-terms.sig for data-type of proof terms)