val binder_to_namedv (b: binder) : Tot namedv
let binder_to_namedv (b : binder) : Tot namedv =
  {
    ppname = b.ppname;
    uniq   = b.uniq;
    sort   = seal b.sort;
  }
val binder_to_namedv (b: binder) : Tot namedv
let binder_to_namedv (b: binder) : Tot namedv =
{ ppname = b.ppname; uniq = b.uniq; sort = seal b.sort }
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.Reflection.V2.Data.Mknamedv_view FStar.Tactics.NamedView.__proj__Mkbinder__item__uniq FStar.Sealed.seal FStar.Reflection.Types.typ FStar.Tactics.NamedView.__proj__Mkbinder__item__sort FStar.Tactics.NamedView.__proj__Mkbinder__item__ppname FStar.Tactics.NamedView.namedv
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 =
val binder_to_namedv (b: binder) : Tot namedv
b: FStar.Tactics.NamedView.binder -> FStar.Tactics.NamedView.namedv