proposition: Lemma CausallyConsistent: forall (p: Syntax.PProg)(h: list N.CExec.Label), N.CExec.history (N.CExec.init p) h -> exists (h': list AExec.Label), AExec.history (AExec.init p) h' /\ N.CExec.ext_hist h = AExec.ext_hist h'.
proof: Proof. apply ExecToAbstExec.CausallyConsistent. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)