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