proposition: Lemma recognizes_loop_to_not_in: forall p L, Recognizes p L -> forall i, Loop (p i) -> ~ L i.
proof: Proof. intros. intros N. apply H in N. apply halt_to_not_loop in H0; auto. eauto using run_to_halt. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop