val namedv_to_term (x: namedv) : Tot term
let namedv_to_term (x : namedv) : Tot term =
  pack (Tv_Var x)
val namedv_to_term (x: namedv) : Tot term
let namedv_to_term (x: namedv) : Tot term =
pack (Tv_Var x)
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.namedv FStar.Tactics.NamedView.pack FStar.Tactics.NamedView.Tv_Var FStar.Tactics.NamedView.term
module FStar.Tactics.V2.SyntaxCoercions

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

[@@coercion]
val namedv_to_term (x: namedv) : Tot term
x: FStar.Tactics.NamedView.namedv -> FStar.Tactics.NamedView.term