proposition: Lemma ExecToSeqExec: forall p h s, CExec.StepStar.step_star (CExec.init p) h s -> exists h' s', SExec.StepStar.step_star (SExec.init) h' s' /\ h' = CExec.eff_hist h.
proof: Proof. intros. assert (A := ExecToSeqExec'). specex_deprem A. eassumption. destruct A as [h' [s' [A1 [A2 _]]]]. exists h'. exists s'. split_all; assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)