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