Bugfixing
Change kick_out_eq to match statement of proof.