proposition: Lemma disjoint_run_true_2_rw: forall p1 p2, Disjoint p1 p2 -> Negative p1 <-> Run p2 true.
proof: Proof. intros. split; intros. { destruct H; intuition. run_simpl_all. } destruct H as [(Ha,Hb)|(Ha,Hb)]; intuition. run_simpl_all. Qed.
imports: Turing Coq.Bool.Bool