proposition: Lemma negator_reject: forall p n, CodeOf (negator p) n -> Run (Call n [[ n ]]) false -> Run (p <[ n, [[ n ]] ]>) true.
proof: Proof. unfold negator. intros p n co Hr. run_simpl_all. inversion_clear Hr. destruct b1; run_simpl_all. assumption. Qed.
imports: Coq.Setoids.Setoid Turing.Turing Turing.LangDec Turing.LangRed