proposition: Lemma CauseConsistent_Prog_LostRing: forall h n, C.Alg.CExec.history (C.Alg.CExec.init C.prog_lost_ring) h -> forall l, List.In l h -> l <> C.Alg.CExec.fault_label n.
proof: Proof. exact C.CauseConsistent_Prog_LostRing. Qed.
imports: Coq(String) Chapar(Predefs KVStore ReflectiveAbstractSemantics)