Idris.ProofSearch
trivial
trivialHoles
proofSearch