Implement proof_mode
functionalities
#682
+373
−27
Open
proof_mode
functionalities
#682