Proof Assistant with Checker