val refs_witness (#app:_) (fc: appfn_call app) (k: app_key app.adm)
 (i: Zeta.SeqAux.seq_index fc.inp_c {k = fst (FStar.Seq.index fc.inp_c i)})
  : Lemma (ensures (refs fc k))
val refs_witness (#app:_) (fc: appfn_call app) (k: app_key app.adm)
 (i: Zeta.SeqAux.seq_index fc.inp_c {k = fst (FStar.Seq.index fc.inp_c i)})
  : Lemma (ensures (refs fc k))
let refs_witness (#app:_) (fc: appfn_call app) (k: app_key app.adm)
 (i: Zeta.SeqAux.seq_index fc.inp_c {k = fst (FStar.Seq.index fc.inp_c i)})
  : Lemma (ensures (refs fc k))
 = let open Zeta.SeqIdx in
   exists_elems_with_prop_intro (of_key k) fc.inp_c i
module Zeta.AppSimulate.Helper

open FStar.Classical
module S = FStar.Seq

open Zeta.Ghost

let app_state_feq_comm_aux (#adm:_) (st1 st2: app_state adm)
  : Lemma (requires (app_state_feq st1 st2))
          (ensures (app_state_feq st2 st1))
  = let aux (k:_)
      : Lemma (ensures (st2 k = st1 k))
      = assert(st1 k = st2 k)
    in
    forall_intro aux

let app_state_feq_commutative (#adm) (st1 st2: app_state adm)
  : Lemma (ensures (app_state_feq st1 st2 <==> app_state_feq st2 st1))
  = introduce (app_state_feq st1 st2) ==> (app_state_feq st2 st1)
    with _. app_state_feq_comm_aux st1 st2;
    introduce (app_state_feq st2 st1) ==> (app_state_feq st1 st2)
    with _. app_state_feq_comm_aux st2 st1

let app_state_feq_transitive_aux (#adm) (st1 st2 st3: app_state adm)
  : Lemma (requires (app_state_feq st1 st2 /\ app_state_feq st2 st3))
          (ensures (app_state_feq st1 st3))
  = let aux(k:_)
      : Lemma (ensures (st1 k = st3 k))
      = assert(st1 k = st2 k);
        assert(st2 k = st3 k)
    in
    forall_intro aux

let app_state_feq_transitive (#adm)  (st1 st2 st3: app_state adm)
  : Lemma (ensures (app_state_feq st1 st2 ==> app_state_feq st2 st3 ==> app_state_feq st1 st3))
  = introduce (app_state_feq st1 st2 /\ app_state_feq st2 st3) ==> (app_state_feq st1 st3)
    with _. app_state_feq_transitive_aux st1 st2 st3

let of_key (#adm:_) (ki: app_key adm) (r: app_record adm)
  = let k,_ = r in
    k = ki
/
Zeta.SeqIdx.fsti.checked Zeta.SeqAux.fsti.checked Zeta.Ghost.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked
Zeta.AppSimulate.Helper.fst

    fc: Zeta.AppSimulate.appfn_call app ->
    k: Zeta.App.app_key (Mkapp_params?.adm app) ->
    i:
      Zeta.SeqAux.seq_index (Mkappfn_call?.inp_c fc)
        {k = FStar.Pervasives.Native.fst (FStar.Seq.Base.index (Mkappfn_call?.inp_c fc) i)}
  -> FStar.Pervasives.Lemma (ensures Zeta.AppSimulate.refs fc k)
Zeta.App.app_params Zeta.AppSimulate.appfn_call Zeta.App.app_key Zeta.App.__proj__Mkapp_params__item__adm Zeta.SeqAux.seq_index Zeta.App.app_record Zeta.AppSimulate.__proj__Mkappfn_call__item__inp_c Prims.b2t Prims.op_Equality FStar.Pervasives.Native.fst Zeta.App.app_value_nullable FStar.Seq.Base.index Zeta.SeqIdx.exists_elems_with_prop_intro Zeta.AppSimulate.Helper.of_key Prims.unit Prims.l_True Prims.squash Zeta.AppSimulate.refs Prims.Nil FStar.Pervasives.pattern
let refs_witness
      (#app: _)
      (fc: appfn_call app)
      (k: app_key app.adm)
      (i: Zeta.SeqAux.seq_index fc.inp_c {k = fst (FStar.Seq.index fc.inp_c i)})
    : Lemma (ensures (refs fc k)) =
  
let open Zeta.SeqIdx in exists_elems_with_prop_intro (of_key k) fc.inp_c i