val global_rel_implies_appfn_identical (#vcfg:_) (gls: verifiable_log vcfg) (glk: _{global_rel gls glk})
  : Lemma (ensures (app_fcrs gls = app_fcrs glk))
val global_rel_implies_appfn_identical (#vcfg:_) (gls: verifiable_log vcfg) (glk: _{global_rel gls glk})
  : Lemma (ensures (app_fcrs gls = app_fcrs glk))
let global_rel_implies_appfn_identical (#vcfg:_) (gls: verifiable_log vcfg) (glk: _{global_rel gls glk})
  : Lemma (ensures (app_fcrs gls = app_fcrs glk))
  = let fcrss = app_fcrs gls in
    let fcrsk = app_fcrs glk in

    assert(S.length fcrss = S.length fcrsk);
    let aux (t:_)
      : Lemma (ensures (S.index fcrss t == S.index fcrsk t))
      = let tls = index gls t in
        let tlk = index glk t in
        eliminate forall t. IT.thread_rel (index gls t) (index glk t)
        with t;
        assert(IT.thread_rel tls tlk);
        IT.thread_rel_implies_fcrs_identical tls tlk
    in
    forall_intro aux;
    assert(S.equal fcrss fcrsk)
module Zeta.Intermediate.Global

open FStar.Classical

module GT = Zeta.Generic.Thread
/
Zeta.Generic.Thread.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked
Zeta.Intermediate.Global.fst

    gls: Zeta.Intermediate.Global.verifiable_log vcfg ->
    glk:
      Zeta.High.Global.verifiable_log (VConfig?.app vcfg)
        {Zeta.Intermediate.Global.global_rel gls glk}
  -> FStar.Pervasives.Lemma
    (ensures Zeta.Generic.Global.app_fcrs gls = Zeta.Generic.Global.app_fcrs glk)
Zeta.Intermediate.VerifierConfig.verifier_config Zeta.Intermediate.Global.verifiable_log Zeta.High.Global.verifiable_log Zeta.Intermediate.VerifierConfig.__proj__VConfig__item__app Zeta.Intermediate.Global.global_rel Prims._assert FStar.Seq.Base.equal FStar.Seq.Base.seq Zeta.AppSimulate.appfn_call_res Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app Zeta.Intermediate.Verifier.int_verifier_spec Prims.unit FStar.Classical.forall_intro Prims.nat Prims.l_and Prims.b2t Prims.op_LessThan FStar.Seq.Base.length Zeta.High.Verifier.high_verifier_spec Prims.eq2 FStar.Seq.Base.index Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern Zeta.Intermediate.Thread.thread_rel_implies_fcrs_identical Zeta.Intermediate.Thread.thread_rel FStar.Classical.Sugar.forall_elim Zeta.GenericVerifier.verifier_log Zeta.Generic.Global.index Zeta.Generic.Thread.verifiable_log Prims.op_Equality Zeta.SSeq.sseq Zeta.Generic.Global.app_fcrs
let global_rel_implies_appfn_identical
      (#vcfg: _)
      (gls: verifiable_log vcfg)
      (glk: _{global_rel gls glk})
    : Lemma (ensures (app_fcrs gls = app_fcrs glk)) =
  
let fcrss = app_fcrs gls in
let fcrsk = app_fcrs glk in
assert (S.length fcrss = S.length fcrsk);
let aux (t: _) : Lemma (ensures (S.index fcrss t == S.index fcrsk t)) =
  let tls = index gls t in
  let tlk = index glk t in
  eliminate forall t. IT.thread_rel (index gls t) (index glk t)
  with t;
  assert (IT.thread_rel tls tlk);
  IT.thread_rel_implies_fcrs_identical tls tlk
in
forall_intro aux;
assert (S.equal fcrss fcrsk)