val bv_eq : bv -> bv -> Tot bool
let bv_eq (bv1 bv2 : bv) =
  let bvv1 = inspect_bv bv1 in
  let bvv2 = inspect_bv bv2 in
  (* We don't check for type equality: the fact that no two different binders
   * have the same name and index is an invariant which must be enforced -
   * and actually we could limit ourselves to checking the index *)
  bvv1.bv_index = bvv2.bv_index
val bv_eq : bv -> bv -> Tot bool
let bv_eq (bv1 bv2: bv) =
let bvv1 = inspect_bv bv1 in
let bvv2 = inspect_bv bv2 in
bvv1.bv_index = bvv2.bv_index
FStar.InteractiveHelpers.Base.fst.checked
prims.fst.checked FStar.Tactics.Util.fst.checked FStar.Tactics.fst.checked FStar.Sealed.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Order.fst.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked
FStar.InteractiveHelpers.Base.fst
FStar.Reflection.Types.bv Prims.op_Equality Prims.nat FStar.Reflection.V1.Data.__proj__Mkbv_view__item__bv_index FStar.Reflection.V1.Data.bv_view Prims.precedes FStar.Reflection.V1.Builtins.inspect_bv Prims.bool
module FStar.InteractiveHelpers.Base

open FStar.List
open FStar.Tactics
open FStar.Mul

#push-options "--z3rlimit 15 --fuel 0 --ifuel 1"

(*** Utilities *)
val bv_eq : bv -> bv -> Tot bool
bv1: FStar.Reflection.Types.bv -> bv2: FStar.Reflection.Types.bv -> Prims.bool