proposition: Lemma CauseConsistent_Prog_PhotoAlbum: forall h n, Alg.CExec.history (Alg.CExec.init prog_photo_album) h -> forall l, List.In l h -> l <> Alg.CExec.fault_label n.
proof: Proof. intros h n Hrun; intros. eapply FaultFreedom; eauto; intros. eapply CausallyContent_Prog_PhotoAlbum; eauto. Qed.
imports: Coq(String) Chapar(Predefs KVStore ReflectiveAbstractSemantics)