Coq OK, I can't resist it anymore! ./run self forward_small backward_small backward_large true false false_case