val eq_list (f: (x: 'a -> y: 'a -> b: bool{b <==> (x == y)})) (l m: list 'a)
    : b: bool{b <==> (l == m)}
let rec eq_list (f: (x:'a -> y:'a -> b:bool { b <==> (x == y)})) (l m:list 'a)
  : b:bool { b <==> (l == m) }
  = match l, m with
    | [], [] -> true
    | h1::t1, h2::t2 ->
      f h1 h2 &&
      eq_list f t1 t2
    | _ -> false
val eq_list (f: (x: 'a -> y: 'a -> b: bool{b <==> (x == y)})) (l m: list 'a)
    : b: bool{b <==> (l == m)}
let rec eq_list (f: (x: 'a -> y: 'a -> b: bool{b <==> (x == y)})) (l m: list 'a)
    : b: bool{b <==> (l == m)} =
match l, m with
| [], [] -> true
| h1 :: t1, h2 :: t2 -> f h1 h2 && eq_list f t1 t2
| _ -> false
Pulse.Syntax.Base.fst.checked
prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Sealed.fsti.checked FStar.Reflection.V2.TermEq.fst.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.Builtins.fsti.checked FStar.Reflection.Typing.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Pulse.Syntax.Base.fst
Prims.bool Prims.l_iff Prims.b2t Prims.eq2 Prims.list FStar.Pervasives.Native.Mktuple2 Prims.op_AmpAmp Pulse.Syntax.Base.eq_list FStar.Pervasives.Native.tuple2
module Pulse.Syntax.Base
module RTB = FStar.Reflection.Typing.Builtins
module RT = FStar.Reflection.Typing
module R = FStar.Reflection.V2
module T = FStar.Tactics.V2

let eq_univ (u1 u2:universe) : b:bool{b <==> u1 == u2} =
  let open FStar.Reflection.V2.TermEq in
  assume (faithful_univ u1);
  assume (faithful_univ u2);
  univ_eq_dec u1 u2

let rec eq_tm (t1 t2:term)
  : Tot (b:bool { b <==> (t1 == t2) }) (decreases t1)
  = match t1.t, t2.t with
    | Tm_VProp, Tm_VProp
    | Tm_Emp, Tm_Emp
    | Tm_Inames, Tm_Inames
    | Tm_EmpInames, Tm_EmpInames
    | Tm_Unknown, Tm_Unknown -> true
    | Tm_Star l1 r1, Tm_Star l2 r2 ->
      eq_tm l1 l2 &&
      eq_tm r1 r2
    | Tm_Pure p1, Tm_Pure p2 ->
      eq_tm p1 p2
    | Tm_ExistsSL u1 t1 b1, Tm_ExistsSL u2 t2 b2
    | Tm_ForallSL u1 t1 b1, Tm_ForallSL u2 t2 b2 ->
      eq_univ u1 u2 &&
      eq_tm t1.binder_ty t2.binder_ty &&
      eq_tm b1 b2
    | Tm_FStar t1, Tm_FStar t2 ->
      let open FStar.Reflection.V2.TermEq in
      assume (faithful t1);
      assume (faithful t2);
      term_eq_dec t1 t2
    | _ -> false

let eq_st_comp (s1 s2:st_comp)  
  : b:bool { b <==> (s1 == s2) }
  = eq_univ s1.u s2.u &&
    eq_tm s1.res s2.res &&
    eq_tm s1.pre s2.pre &&
    eq_tm s1.post s2.post

let eq_comp (c1 c2:comp)
  : b:bool { b <==> (c1 == c2) }
  = match c1, c2 with
    | C_Tot t1, C_Tot t2 ->
      eq_tm t1 t2
    | C_ST s1, C_ST s2 ->
      eq_st_comp s1 s2
    | C_STAtomic i1 s1, C_STAtomic i2 s2
    | C_STGhost i1 s1, C_STGhost i2 s2 ->
      eq_tm i1 i2 &&
      eq_st_comp s1 s2
    | _ -> false

let rec eq_list (f: (x:'a -> y:'a -> b:bool { b <==> (x == y)})) (l m:list 'a)
val eq_list (f: (x: 'a -> y: 'a -> b: bool{b <==> (x == y)})) (l m: list 'a)
    : b: bool{b <==> (l == m)}
f: (x: 'a -> y: 'a -> b: Prims.bool{b <==> x == y}) -> l: Prims.list 'a -> m: Prims.list 'a
  -> b: Prims.bool{b <==> l == m}