proposition: Lemma run_true_or_negative: forall p, Run p true \/ Negative p.
proof: Proof. intros. destruct (run_exists p) as [([], H)|H]; auto; right; auto using negative_run_false, negative_loop. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop