diff --git a/src/3d/prelude/EverParse3d.Actions.Base.fst b/src/3d/prelude/EverParse3d.Actions.Base.fst
index 27f4e4fb0..854ecd7e4 100644
--- a/src/3d/prelude/EverParse3d.Actions.Base.fst
+++ b/src/3d/prelude/EverParse3d.Actions.Base.fst
@@ -55,7 +55,7 @@ let input_buffer_t = EverParse3d.InputStream.All.t
 let action
   p inv l on_success a
 =
-    (# [tcresolve ()] I.extra_t #input_buffer_t) ->
+    (# [EverParse3d.Util.solve_from_ctx ()] I.extra_t #input_buffer_t) ->
     ctxt: app_ctxt ->
     sl: input_buffer_t ->
     pos: LPE.pos_t ->
@@ -160,7 +160,7 @@ let error_handler =
 
 inline_for_extraction noextract
 let validate_with_action_t' (#k:LP.parser_kind) (#t:Type) (p:LP.parser k t) (inv:slice_inv) (l:eloc) (allow_reading:bool) =
-  (# [tcresolve ()] I.extra_t #input_buffer_t) ->
+  (# [EverParse3d.Util.solve_from_ctx ()] I.extra_t #input_buffer_t) ->
   (ctxt: app_ctxt) ->
   (error_handler_fn : error_handler) ->
   (sl: input_buffer_t) ->
@@ -216,7 +216,7 @@ let leaf_reader
   (p: parser k t)
 : Tot Type
 =
-  (# [FStar.Tactics.Typeclasses.tcresolve ()] _extra_t : I.extra_t #input_buffer_t ) ->
+  (# [EverParse3d.Util.solve_from_ctx ()] _extra_t : I.extra_t #input_buffer_t ) ->
   (sl: input_buffer_t) ->
   (pos: LPE.pos_t) ->
   Stack t
@@ -825,7 +825,7 @@ let validate_list_inv
 inline_for_extraction
 noextract
 let validate_list_body
-  (# [FStar.Tactics.Typeclasses.tcresolve ()] _extra_t : I.extra_t #input_buffer_t ) 
+  (# [EverParse3d.Util.solve_from_ctx ()] _extra_t : I.extra_t #input_buffer_t )
   (#k:LP.parser_kind)
   #t
   (#p:LP.parser k t)
@@ -860,7 +860,7 @@ let validate_list_body
 inline_for_extraction
 noextract
 let validate_list'
-  (# [FStar.Tactics.Typeclasses.tcresolve ()] _extra_t : I.extra_t #input_buffer_t ) 
+  (# [EverParse3d.Util.solve_from_ctx ()] _extra_t : I.extra_t #input_buffer_t )
   (#k:LP.parser_kind)
   #t
   (#p:LP.parser k t)
@@ -1505,7 +1505,7 @@ let validate_list_up_to_inv
 
 inline_for_extraction
 let validate_list_up_to_body
-  (# [FStar.Tactics.Typeclasses.tcresolve ()] _extra_t : I.extra_t #input_buffer_t ) 
+  (# [EverParse3d.Util.solve_from_ctx ()] _extra_t : I.extra_t #input_buffer_t )
   (#k: parser_kind true WeakKindStrongPrefix)
   (#t: eqtype)
   (#p: parser k t)
diff --git a/src/3d/prelude/EverParse3d.InputStream.All.fsti b/src/3d/prelude/EverParse3d.InputStream.All.fsti
index 24eab2b93..69c32a626 100644
--- a/src/3d/prelude/EverParse3d.InputStream.All.fsti
+++ b/src/3d/prelude/EverParse3d.InputStream.All.fsti
@@ -7,7 +7,6 @@ inline_for_extraction
 noextract
 val t : Type0
 
-[@@FStar.Tactics.Typeclasses.tcinstance]
 inline_for_extraction
 noextract
-val inst : input_stream_inst t
+instance val inst : input_stream_inst t
diff --git a/src/3d/prelude/EverParse3d.InputStream.Base.fst b/src/3d/prelude/EverParse3d.InputStream.Base.fst
index 4838e1644..a69bbb226 100644
--- a/src/3d/prelude/EverParse3d.InputStream.Base.fst
+++ b/src/3d/prelude/EverParse3d.InputStream.Base.fst
@@ -61,7 +61,7 @@ class input_stream_inst (t: Type) : Type = {
   extra_t: Type0;
 
   has:
-    (# [FStar.Tactics.Typeclasses.tcresolve () ] extra_t ) ->
+    (# [EverParse3d.Util.solve_from_ctx () ] extra_t ) ->
     (x: t) ->
     (len: tlen x) ->
     (pos: LPE.pos_t) ->
@@ -77,7 +77,7 @@ class input_stream_inst (t: Type) : Type = {
     ));
   
   read:
-    (# [FStar.Tactics.Typeclasses.tcresolve ()] extra_t ) ->
+    (# [EverParse3d.Util.solve_from_ctx ()] extra_t ) ->
     (t': Type0) ->
     (k: LP.parser_kind) ->
     (p: LP.parser k t') ->
@@ -107,7 +107,7 @@ class input_stream_inst (t: Type) : Type = {
     ));
 
   skip:
-    (# [FStar.Tactics.Typeclasses.tcresolve ()] extra_t ) ->
+    (# [EverParse3d.Util.solve_from_ctx ()] extra_t ) ->
     (x: t) ->
     (pos: LPE.pos_t) ->
     (n: U64.t) ->
@@ -125,7 +125,7 @@ class input_stream_inst (t: Type) : Type = {
     ));
 
   skip_if_success:
-    (# [FStar.Tactics.Typeclasses.tcresolve ()] extra_t ) ->
+    (# [EverParse3d.Util.solve_from_ctx ()] extra_t ) ->
     (x: t) ->
     (pos: LPE.pos_t) ->
     (res: U64.t) ->
@@ -145,7 +145,7 @@ class input_stream_inst (t: Type) : Type = {
     ));
   
   empty:
-    (# [FStar.Tactics.Typeclasses.tcresolve ()] extra_t ) ->
+    (# [EverParse3d.Util.solve_from_ctx ()] extra_t ) ->
     (x: t) ->
     (len: tlen x) ->
     (pos: LPE.pos_t) ->
@@ -233,7 +233,7 @@ let length_all #t (#_: input_stream_inst t) (x: t) : GTot nat = U64.v (len_all x
 
 let preserved'
     (#t: Type)
-    (# [FStar.Tactics.Typeclasses.tcresolve ()] inst : input_stream_inst t)
+    (# [EverParse3d.Util.solve_from_ctx ()] inst : input_stream_inst t)
     (x: t)
     (l: B.loc)
     (h: HS.mem)
diff --git a/src/3d/prelude/EverParse3d.Util.fst b/src/3d/prelude/EverParse3d.Util.fst
new file mode 100644
index 000000000..6886ee32d
--- /dev/null
+++ b/src/3d/prelude/EverParse3d.Util.fst
@@ -0,0 +1,8 @@
+module EverParse3d.Util
+
+open FStar.Tactics.V2
+
+let solve_from_ctx () : Tac unit =
+  ignore (intros ());
+  let bs = vars_of_env (cur_env ()) in
+  first (map (fun (b:binding) () -> exact b) bs)
diff --git a/src/3d/prelude/buffer/EverParse3d.InputStream.Buffer.fsti b/src/3d/prelude/buffer/EverParse3d.InputStream.Buffer.fsti
index f4bfdb9cb..614c32087 100644
--- a/src/3d/prelude/buffer/EverParse3d.InputStream.Buffer.fsti
+++ b/src/3d/prelude/buffer/EverParse3d.InputStream.Buffer.fsti
@@ -12,7 +12,6 @@ inline_for_extraction
 noextract
 val t : Type0
 
-[@@ FStar.Tactics.Typeclasses.tcinstance]
 noextract
 inline_for_extraction
-val inst : input_stream_inst t
+instance val inst : input_stream_inst t
diff --git a/src/3d/prelude/extern/EverParse3d.InputStream.Extern.Base.fsti b/src/3d/prelude/extern/EverParse3d.InputStream.Extern.Base.fsti
index c9920677e..af17feaa6 100644
--- a/src/3d/prelude/extern/EverParse3d.InputStream.Extern.Base.fsti
+++ b/src/3d/prelude/extern/EverParse3d.InputStream.Extern.Base.fsti
@@ -60,7 +60,7 @@ val preserved:
 val extra_t: Type0
 
 val has:
-    (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: extra_t) ->
+    (#[EverParse3d.Util.solve_from_ctx ()] _extra_t: extra_t) ->
     (x: t) ->
     (n: U64.t) ->
     HST.Stack bool
@@ -71,7 +71,7 @@ val has:
     ))
 
 val read:
-    (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: extra_t) ->
+    (#[EverParse3d.Util.solve_from_ctx ()] _extra_t: extra_t) ->
     (x: t) ->
     (n: U64.t) ->
     (dst: B.buffer U8.t) ->
@@ -96,7 +96,7 @@ val read:
 
 noextract [@@noextract_to "krml"]
 let peep_pre
-    (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: extra_t)
+    (#[EverParse3d.Util.solve_from_ctx ()] _extra_t: extra_t)
     (x: t)
     (n: U64.t)
     (h: HS.mem)
@@ -107,7 +107,7 @@ let peep_pre
 
 noextract [@@noextract_to "krml"]
 let peep_post
-    (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: extra_t)
+    (#[EverParse3d.Util.solve_from_ctx ()] _extra_t: extra_t)
     (x: t)
     (n: U64.t)
     (h: HS.mem)
@@ -127,7 +127,7 @@ let peep_post
   end
 
 val peep:
-    (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: extra_t) ->
+    (#[EverParse3d.Util.solve_from_ctx ()] _extra_t: extra_t) ->
     (x: t) ->
     (n: U64.t) ->
     HST.Stack (B.buffer U8.t)
@@ -139,7 +139,7 @@ val peep:
     ))
 
 val skip:
-    (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: extra_t) ->
+    (#[EverParse3d.Util.solve_from_ctx ()] _extra_t: extra_t) ->
     (x: t) ->
     (n: U64.t) ->
     HST.Stack unit
@@ -152,7 +152,7 @@ val skip:
     ))
 
 val empty:
-    (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: extra_t) ->
+    (#[EverParse3d.Util.solve_from_ctx ()] _extra_t: extra_t) ->
     (x: t) ->
     HST.Stack U64.t
     (requires (fun h -> live x h))
diff --git a/src/3d/prelude/extern/EverParse3d.InputStream.Extern.fst b/src/3d/prelude/extern/EverParse3d.InputStream.Extern.fst
index 045421cc3..e5f49ea79 100644
--- a/src/3d/prelude/extern/EverParse3d.InputStream.Extern.fst
+++ b/src/3d/prelude/extern/EverParse3d.InputStream.Extern.fst
@@ -111,7 +111,7 @@ open LowStar.BufferOps
 inline_for_extraction
 noextract
 let has
-    (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
+    (#[EverParse3d.Util.solve_from_ctx ()] _extra_t: Aux.extra_t)
     (x: t)
     (_: unit)
     (position: LPE.pos_t)
@@ -137,7 +137,7 @@ let has
 inline_for_extraction
 noextract
 let read0
-    (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
+    (#[EverParse3d.Util.solve_from_ctx ()] _extra_t: Aux.extra_t)
     (x: t)
     (position: LPE.pos_t)
     (n: U64.t)
@@ -183,7 +183,7 @@ module LP = LowParse.Low.Base
 inline_for_extraction
 noextract
 let read
-    (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
+    (#[EverParse3d.Util.solve_from_ctx ()] _extra_t: Aux.extra_t)
     (t': Type0)
     (k: LP.parser_kind)
     (p: LP.parser k t')
@@ -245,7 +245,7 @@ let read
 
 noextract [@@noextract_to "krml"]
 let peep_pre'
-    (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
+    (#[EverParse3d.Util.solve_from_ctx ()] _extra_t: Aux.extra_t)
     (x: t)
     (position: LPE.pos_t)
     (h: HS.mem)
@@ -257,7 +257,7 @@ let peep_pre'
 noextract [@@noextract_to "krml"]
 unfold
 let peep_post'
-    (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
+    (#[EverParse3d.Util.solve_from_ctx ()] _extra_t: Aux.extra_t)
     (x: t)
     (position: LPE.pos_t)
     (n: U64.t)
@@ -279,7 +279,7 @@ let peep_post'
 
 noextract [@@noextract_to "krml"]
 let peep0_pre'
-    (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
+    (#[EverParse3d.Util.solve_from_ctx ()] _extra_t: Aux.extra_t)
     (x: t)
     (position: LPE.pos_t)
     (n: U64.t)
@@ -292,7 +292,7 @@ let peep0_pre'
 // #restart-solver
 
 let peep_post_extract_concl
-    (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
+    (#[EverParse3d.Util.solve_from_ctx ()] _extra_t: Aux.extra_t)
     (x: Aux.t)
     (n: U64.t)
     (h: HS.mem)
@@ -316,7 +316,7 @@ let peep_post_extract_concl
 = ()
 
 let peep0_exit // this is the crucial lemma for peep to work
-    (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
+    (#[EverParse3d.Util.solve_from_ctx ()] _extra_t: Aux.extra_t)
     (x: t)
     (position: LPE.pos_t)
     (n: U64.t)
@@ -350,7 +350,7 @@ let peep0_exit // this is the crucial lemma for peep to work
 inline_for_extraction
 noextract
 let peep0
-    (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
+    (#[EverParse3d.Util.solve_from_ctx ()] _extra_t: Aux.extra_t)
     (x: t)
     (position: LPE.pos_t)
     (n: U64.t)
@@ -363,7 +363,7 @@ let peep0
 inline_for_extraction
 noextract
 let peep
-    (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
+    (#[EverParse3d.Util.solve_from_ctx ()] _extra_t: Aux.extra_t)
     (x: t)
     (position: LPE.pos_t)
     (n: U64.t)
@@ -385,7 +385,7 @@ let peep
 inline_for_extraction
 noextract
 let skip
-    (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
+    (#[EverParse3d.Util.solve_from_ctx ()] _extra_t: Aux.extra_t)
     (x: t)
     (position: LPE.pos_t)
     (n: U64.t)
@@ -410,7 +410,7 @@ let skip
 inline_for_extraction
 noextract
 let skip_if_success
-    (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
+    (#[EverParse3d.Util.solve_from_ctx ()] _extra_t: Aux.extra_t)
     (x: t)
     (pos: LPE.pos_t)
     (res: U64.t)
@@ -436,7 +436,7 @@ let skip_if_success
 inline_for_extraction
 noextract
 let empty
-    (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
+    (#[EverParse3d.Util.solve_from_ctx ()] _extra_t: Aux.extra_t)
     (x: t)
     (_: unit)
     (position: LPE.pos_t)