val app_state_feq_commutative (#adm:_) (st1 st2: app_state adm)
  : Lemma (ensures (app_state_feq st1 st2 <==> app_state_feq st2 st1))
          [SMTPat (app_state_feq st1 st2); SMTPat (app_state_feq st2 st1)]
val app_state_feq_commutative (#adm:_) (st1 st2: app_state adm)
  : Lemma (ensures (app_state_feq st1 st2 <==> app_state_feq st2 st1))
          [SMTPat (app_state_feq st1 st2); SMTPat (app_state_feq st2 st1)]
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
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
/
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
st1: Zeta.AppSimulate.app_state adm -> st2: Zeta.AppSimulate.app_state adm
  -> FStar.Pervasives.Lemma
      (ensures
        Zeta.AppSimulate.Helper.app_state_feq st1 st2 <==>
        Zeta.AppSimulate.Helper.app_state_feq st2 st1)
      [
        SMTPat (Zeta.AppSimulate.Helper.app_state_feq st1 st2);
        SMTPat (Zeta.AppSimulate.Helper.app_state_feq st2 st1)
      ]
Zeta.App.app_data_model Zeta.AppSimulate.app_state FStar.Classical.Sugar.implies_intro Zeta.AppSimulate.Helper.app_state_feq Prims.squash Zeta.AppSimulate.Helper.app_state_feq_comm_aux Prims.unit Prims.l_True Prims.l_iff Prims.Nil FStar.Pervasives.pattern
let app_state_feq_commutative #adm (st1: app_state adm) (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