proposition: Lemma run_seq_pre_rw {p} {b'}: Run p b' -> forall q b , Run (Seq p q) b <-> Run (q b') b.
proof: Proof. intros. rewrite run_seq_rw. split; intros. { destruct H0 as (b1, (Hr1, Hr2)). assert (b' = b1) by eauto using run_fun. subst. assumption. } exists b'. intuition. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop