proposition: Lemma negative_rw: forall p, Negative p <-> ~ Run p true.
proof: Proof. split; intros. { intros N. inversion_clear H. { assert (X: true = false) by eauto using run_fun. inversion X. } rewrite loop_rw in *. contradict H0. eapply run_to_halt; eauto. } destruct (halt_or_loop p). { rewrite halt_rw in *. destruct H0 as ([], Ha); try contradiction. auto using negative_run_false. } auto using negative_loop. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop