val binder_to_term (b: binder) : Tot term
let binder_to_term (b : binder) : Tot term =
  pack (Tv_Var (binder_to_namedv b))
val binder_to_term (b: binder) : Tot term
let binder_to_term (b: binder) : Tot term =
pack (Tv_Var (binder_to_namedv b))
FStar.Tactics.V2.SyntaxCoercions.fst.checked
prims.fst.checked FStar.Tactics.NamedView.fsti.checked FStar.Tactics.Builtins.fst.checked FStar.Sealed.fsti.checked FStar.Pervasives.fsti.checked
FStar.Tactics.V2.SyntaxCoercions.fst
FStar.Tactics.NamedView.binder FStar.Tactics.NamedView.pack FStar.Tactics.NamedView.Tv_Var FStar.Tactics.V2.SyntaxCoercions.binder_to_namedv FStar.Tactics.NamedView.term
module FStar.Tactics.V2.SyntaxCoercions

open FStar.Tactics.Builtins
open FStar.Tactics.NamedView
open FStar.Sealed

[@@coercion]
let namedv_to_term (x : namedv) : Tot term =
  pack (Tv_Var x)

[@@coercion]
let binder_to_namedv (b : binder) : Tot namedv =
  {
    ppname = b.ppname;
    uniq   = b.uniq;
    sort   = seal b.sort;
  }

[@@coercion]
val binder_to_term (b: binder) : Tot term
b: FStar.Tactics.NamedView.binder -> FStar.Tactics.NamedView.term