val empty_log_implies_init_state
  (#app: _)
  (k: base_key)
  (l: vlog_ext app{length l = 0})
  : Lemma (ensures (eac_state_of_key k l = EACInit))
val empty_log_implies_init_state
  (#app: _)
  (k: base_key)
  (l: vlog_ext app{length l = 0})
  : Lemma (ensures (eac_state_of_key k l = EACInit))
let empty_log_implies_init_state
  (#app: _)
  (k: base_key)
  (l: vlog_ext app{length l = 0})
  : Lemma (ensures (eac_state_of_key k l = EACInit))
  = let smk = eac_smk app k in
    lemma_empty_seq_init smk l
module Zeta.EAC

open FStar.Classical

open Zeta.SeqMachine
open Zeta.SeqAux
/
Zeta.SeqMachine.fsti.checked Zeta.SeqIdx.fsti.checked Zeta.SeqAux.fsti.checked Zeta.Record.fsti.checked Zeta.BinTree.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked
Zeta.EAC.fst
k: Zeta.GenericVerifier.base_key -> l: Zeta.EAC.vlog_ext app {FStar.Seq.Base.length l = 0}
  -> FStar.Pervasives.Lemma (ensures Zeta.EAC.eac_state_of_key k l = Zeta.EAC.EACInit)
Zeta.App.app_params Zeta.GenericVerifier.base_key Zeta.EAC.vlog_ext Prims.b2t Prims.op_Equality Prims.int FStar.Seq.Base.length Zeta.EAC.vlog_entry_ext Zeta.SeqMachine.lemma_empty_seq_init Zeta.SeqMachine.seq_machine Zeta.EAC.eac_smk Prims.unit Prims.l_True Prims.squash Zeta.EAC.eac_state Zeta.EAC.eac_state_of_key Zeta.EAC.EACInit Prims.Nil FStar.Pervasives.pattern
let empty_log_implies_init_state (#app: _) (k: base_key) (l: vlog_ext app {length l = 0})
    : Lemma (ensures (eac_state_of_key k l = EACInit)) =
  
let smk = eac_smk app k in
lemma_empty_seq_init smk l