let term_eq = FStar.Tactics.term_eq_old
let term_eq =
FStar.Tactics.term_eq_old
FStar.InteractiveHelpers.Propositions.fst.checked
prims.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.fst.checked FStar.InteractiveHelpers.ExploreTerm.fst.checked FStar.InteractiveHelpers.Base.fst.checked
FStar.InteractiveHelpers.Propositions.fst
FStar.Tactics.V1.Builtins.term_eq_old
module FStar.InteractiveHelpers.Propositions

open FStar.List
open FStar.Tactics
open FStar.Mul
open FStar.InteractiveHelpers.Base
open FStar.InteractiveHelpers.ExploreTerm
val term_eq : _: FStar.Reflection.Types.term -> _: FStar.Reflection.Types.term
  -> FStar.Tactics.Effect.Tac Prims.bool
_: FStar.Reflection.Types.term -> _: FStar.Reflection.Types.term
  -> FStar.Tactics.Effect.Tac Prims.bool