val app_state_feq : st1: Zeta.AppSimulate.app_state adm -> st2: Zeta.AppSimulate.app_state adm -> Prims.logical
let app_state_feq #adm (st1 st2: app_state adm)
  = forall (k: app_key adm). {:pattern (st1 k = st2 k)} st1 k = st2 k
module Zeta.AppSimulate.Helper

open Zeta.App
open Zeta.AppSimulate

(* Helper lemmas for reasoning about app simulate *)
/
Zeta.SeqAux.fsti.checked Zeta.AppSimulate.fsti.checked Zeta.App.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Zeta.AppSimulate.Helper.fsti
st1: Zeta.AppSimulate.app_state adm -> st2: Zeta.AppSimulate.app_state adm -> Prims.logical
Zeta.App.app_data_model Zeta.AppSimulate.app_state Prims.l_Forall Zeta.App.app_key Prims.b2t Prims.op_Equality Zeta.App.app_value_nullable Prims.logical
let app_state_feq #adm (st1: app_state adm) (st2: app_state adm) =
  
forall (k: app_key adm). {:pattern (st1 k = st2 k)} st1 k = st2 k