A Proof Assistant Prototype Based on Algebraic Effects and Handlers