Proof Assistant with Solver