proposition: Lemma run_seq_rw: forall p q b, Run (Seq p q) b <-> ( (exists b', Run p b' /\ Run (q b') b) ).
proof: Proof. split; intros. { inversion_clear H. destruct b; exists b1; intuition. } destruct H as (b', (Ha,Hb)). econstructor; eauto. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop