proposition: Lemma apply_log_app : forall h d entries e, apply_log h d (entries ++ [e]) = apply_entry h (apply_log h d entries) e.
proof: Proof. Proof using. intros. unfold apply_log. rewrite fold_left_app. reflexivity. Qed.
imports: Verdi(Verdi) Cheerios(Cheerios) Verdi(Log) Coq(FunctionalExtensionality)