proposition: Lemma negative_alt_rw: forall p, Negative p <-> (Run p false \/ Loop p).
proof: Proof. split; intros. { inversion_clear H; auto. } destruct H. { auto using negative_run_false. } auto using negative_loop. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop