Idris.ProofSearch
trivial
proofSearch