diff --git a/apps/tc-tabled/elpi/assoc.elpi b/apps/tc-tabled/elpi/assoc.elpi
new file mode 100644
index 000000000..aa07acbe0
--- /dev/null
+++ b/apps/tc-tabled/elpi/assoc.elpi
@@ -0,0 +1,184 @@
+namespace avl {
+% -----------------------------------------
+% Types
+% -----------------------------------------
+
+kind tree type -> type -> type.
+type nil tree K V.
+type node tree K V -> K -> V -> int -> tree K V -> tree K V.
+
+kind cmp type.
+type lt cmp.
+type eq cmp.
+type gt cmp.
+
+% -----------------------------------------
+% Utilities
+% -----------------------------------------
+
+pred max i:int, i:int, o:int.
+max X Y X :- X >= Y.
+max X Y Y :- X < Y.
+
+pred height i:tree K V, o:int.
+height (nil) 0.
+height (node _ _ _ H _) H.
+
+pred balanceFactor i:tree K V, o:int.
+balanceFactor (nil) 0.
+balanceFactor (node L _ _ _ R) BF :-
+  height L HL,
+  height R HR,
+  BF is HL - HR.
+
+% -----------------------------------------
+% Rotations
+% -----------------------------------------
+
+pred rotateLeft i:tree K V, o:tree K V.
+rotateLeft (node L K V _ (node RL RK RV _ RR)) TOut :-
+  height L HL,
+  height RL HRL,
+  max HL HRL LMax,
+  HL1 is LMax + 1,
+  height RR HRR,
+  max HRL HRR RMax,
+  HR1 is RMax + 1,
+  TOut = node (node L K V HL1 RL) RK RV HR1 RR.
+
+pred rotateRight i:tree K V, o:tree K V.
+rotateRight (node (node LL LK LV _ LR) K V _ R) TOut :-
+  height LL HLL,
+  height LR HLR,
+  max HLL HLR LMax,
+  HL1 is LMax + 1,
+  height R HR,
+  max HLR HR RMax,
+  HR1 is RMax + 1,
+  TOut = node LL LK LV HL1 (node LR K V HR1 R).
+
+% -----------------------------------------
+% Balancing
+% -----------------------------------------
+
+pred balance i:tree K V, o:tree K V.
+balance (nil) (nil).
+balance (node L K V _ R) TOut :-
+  height L HL,
+  height R HR,
+  BF is HL - HR,
+  if (BF > 1)
+    (
+      balanceFactor L BFL,
+      if (BFL >= 0)
+        ( rotateRight (node L K V 0 R) TOut )
+        ( rotateLeft L L1, rotateRight (node L1 K V 0 R) TOut )
+    )
+    ( if (BF < -1)
+        (
+          balanceFactor R BFR,
+          if (BFR =< 0)
+            ( rotateLeft (node L K V 0 R) TOut )
+            ( rotateRight R R1, rotateLeft (node L K V 0 R1) TOut )
+        )
+        (
+          max HL HR M,
+          H is M + 1,
+          TOut = node L K V H R
+        )
+    ).
+
+% -----------------------------------------
+% Insertion
+% -----------------------------------------
+
+pred insert
+  i:(pred i:K, i:K, o:cmp),
+  i:K, i:V, i:tree K V, o:tree K V.
+
+insert _ K V (nil) (node (nil) K V 1 (nil)).
+insert Cmp K V (node L K0 V0 H R) TOut :-
+  Cmp K K0 Ord,
+  if (Ord = lt)
+    (
+      insert Cmp K V L L1,
+      height L1 HL,
+      height R HR,
+      max HL HR M,
+      H1 is M + 1,
+      balance (node L1 K0 V0 H1 R) TOut
+    )
+    ( if (Ord = gt)
+        (
+          insert Cmp K V R R1,
+          height L HL,
+          height R1 HR,
+          max HL HR M,
+          H1 is M + 1,
+          balance (node L K0 V0 H1 R1) TOut
+        )
+        ( % eq = update value
+          height L HL,
+          height R HR,
+          max HL HR M,
+          H1 is M + 1,
+          balance (node L K V H1 R) TOut
+        )
+    ).
+
+% -----------------------------------------
+% Update
+% -----------------------------------------
+
+pred update
+  i:(pred i:K, i:K, o:cmp),
+  i:K, i:V, i:tree K V, o:tree K V.
+
+update _ K V (nil) (node (nil) K V 1 (nil)).
+update Cmp K V (node L K0 V0 H R) TOut :-
+  Cmp K K0 Ord,
+  if (Ord = lt)
+    (
+      update Cmp K V L L1,
+      height L1 HL,
+      height R HR,
+      max HL HR M,
+      H1 is M + 1,
+      balance (node L1 K0 V0 H1 R) TOut
+    )
+    ( if (Ord = gt)
+        (
+          update Cmp K V R R1,
+          height L HL,
+          height R1 HR,
+          max HL HR M,
+          H1 is M + 1,
+          balance (node L K0 V0 H1 R1) TOut
+        )
+        ( % eq = update value
+          height L HL,
+          height R HR,
+          max HL HR M,
+          H1 is M + 1,
+          balance (node L K V H1 R) TOut
+        )
+    ).
+
+pred lookup
+  i:(pred i:K, i:K, o:cmp),
+  i:K,
+  i:tree K V,
+  o:V.
+
+lookup _ _ (nil) _ :- fail. % key not found
+
+lookup Cmp K (node L K0 V0 _ R) V :-
+  Cmp K K0 Ord,
+  if (Ord = lt)
+    ( lookup Cmp K L V )
+    ( if (Ord = gt)
+        ( lookup Cmp K R V )
+        ( V = V0 ) % eq
+    ).
+
+}
\ No newline at end of file
diff --git a/apps/tc-tabled/elpi/custom_map.elpi b/apps/tc-tabled/elpi/custom_map.elpi
new file mode 100644
index 000000000..c31e53bdc
--- /dev/null
+++ b/apps/tc-tabled/elpi/custom_map.elpi
@@ -0,0 +1,63 @@
+pred binary_search i:K i:(pred i:K i:K o:cmp) i:int i:int i:list K o:int o:bool.
+binary_search A Cmp L R XS Out Approx :-
+  if (le_ L R)
+   	(M is L + ((R - L) div 2),
+   	std.nth M XS X,
+   	Cmp X A C,
+    !,
+   	if (C = lt)
+ 	     (!, binary_search A Cmp (M + 1) R XS Out Approx)
+ 	     (if (C = gt)
+ 	         (!, binary_search A Cmp L (M - 1) XS Out Approx)
+ 	         (!, Out is M, Approx = ff)))
+ 	  (Out is L, Approx = tt)
+    , !.
+
+kind custom_map type -> type -> type.
+type custom_map list (pair K V) -> (pred i:K i:K o:cmp) -> custom_map K V.
+
+pred custom_make i:(pred i:K, i:K, o:cmp), o:custom_map K V.
+custom_make Cmp (custom_map [] Cmp).
+
+pred cmp_fst_pair i:(pred i:K i:K o:cmp) i:pair K V i:pair K V o:cmp.
+cmp_fst_pair Cmp (pr K1 _) (pr K2 _) C :- Cmp K1 K2 C.
+
+pred custom_find i:K, i:custom_map K V, o:V.
+custom_find K (custom_map M Cmp) V :-
+  std.length M Len,
+  binary_search (pr K (_ /* dummy value */)) (cmp_fst_pair Cmp) 0 (Len - 1) M I ff,
+  !,
+  std.nth I M (pr KK V),
+  Cmp KK K eq,
+  !.
+
+pred insert_index i:int i:V i:list V o:list V.
+%% insert_index I V L O :- /* std.append F [ (pr K VI) | T  ] M1 */
+%%   std.split-at I L F T,
+%%   !,
+%%   std.append F [ V | T ] O.
+insert_index 0 V L [ V | L ].
+insert_index N V [ X | L ] [ X | O ] :-
+  NN is N - 1,
+  insert_index NN V L O.
+
+pred update_index i:int i:V i:list V o:list V.
+%% update_index I V L O :- /* T = [ pr KK _ | VS ] , Cmp KK K eq , std.append F [ (pr K VI) | VS ] M1 */
+%%   std.split-at I L F [ _ | T ],
+%%   !,
+%%   std.append F [ V | T ] O.
+update_index 0 V [ _ | L ] [ V | L ] :- !.
+update_index N V [ X | L ] [ X | O ] :-
+  NN is N - 1,
+  !,
+  update_index NN V L O,
+  !.
+
+pred custom_add i:K, i:V, i:custom_map K V, o:custom_map K V.
+custom_add K V (custom_map M Cmp) (custom_map M1 Cmp) :-
+  std.length M Len,
+  binary_search (pr K (_ /* dummy value */)) (cmp_fst_pair Cmp) 0 (Len - 1) M I Approx,
+  if (Approx = tt)
+     (insert_index I (pr K V) M M1) /* insert */
+     (update_index I (pr K V) M M1 ) /* update */
+  , !.
diff --git a/apps/tc-tabled/elpi/dune b/apps/tc-tabled/elpi/dune
new file mode 100644
index 000000000..16c639362
--- /dev/null
+++ b/apps/tc-tabled/elpi/dune
@@ -0,0 +1,19 @@
+(coq.theory
+ (name elpi.apps.tc_tabled.elpi)
+ (package rocq-elpi)
+ (theories elpi))
+
+(rule
+ (target dummy.v)
+ (deps
+  (glob_files *.elpi))
+ (action
+  (with-stdout-to %{target}
+   (progn
+     (run rocq_elpi_shafile %{deps})))))
+
+(install
+ (files
+  (glob_files (*.elpi with_prefix coq/user-contrib/elpi/apps/tc-tabled/elpi/)))
+ (section lib_root)
+ (package rocq-elpi))
diff --git a/apps/tc-tabled/elpi/map2.elpi b/apps/tc-tabled/elpi/map2.elpi
new file mode 100644
index 000000000..2a8a54449
--- /dev/null
+++ b/apps/tc-tabled/elpi/map2.elpi
@@ -0,0 +1,135 @@
+kind std.map2 type -> type -> type.
+type std.map2 std.map2.private.map K V -> (pred i:K, i:K, o:cmp) -> std.map2 K V.
+
+namespace std.map2 {
+
+  % [make Eq Ltn M] builds an empty map M where keys are compared using Eq and Ltn
+  pred make i:(pred i:K, i:K, o:cmp), o:std.map2 K V.
+  make Cmp (std.map2 private.empty Cmp).
+
+  % [find K M V] looks in M for the value V associated to K
+  pred find i:K, i:std.map2 K V, o:V.
+  find K (std.map2 M Cmp) V :- private.find M Cmp K V.
+
+  % [add K V M M1] M1 is M where K is bound to V
+  pred add i:K, i:V, i:std.map2 K V, o:std.map2 K V.
+  add K V (std.map2 M Cmp) (std.map2 M1 Cmp) :-
+    private.add M Cmp K VV M1,
+    VV = V.
+
+  % [update K V M M1] M1 is M where K is bound to V
+  pred update i:K, i:V, i:std.map2 K V, o:std.map2 K V.
+  update K V (std.map2 M Cmp) (std.map2 M1 Cmp) :-
+    private.update M Cmp K V M1.
+
+  % [remove K M M1] M1 is M where K is unbound
+  pred remove i:K, i:std.map2 K V, o:std.map2 K V.
+  remove K (std.map2 M Cmp) (std.map2 M1 Cmp) :- private.remove M Cmp K M1.
+
+  % [bindings M L] L is the key-value pairs in increasing order
+  pred bindings i:std.map2 K V, o:list (pair K V).
+  bindings (std.map2 M _) L :- private.bindings M [] L.
+
+  namespace private {
+
+    % Taken from OCaml's map.ml
+    kind map type -> type -> type.
+    type empty map K V.
+    type node map K V -> K -> V -> map K V -> int -> map K V.
+
+    pred height i:map K V, o:int.
+    height empty 0.
+    height (node _ _ _ _ H) H.
+
+    pred create i:map K V, i:K, i:V, i:map K V, o:map K V.
+    create L K V R (node L K V R H) :- H is {std.max {height L} {height R} } + 1.
+
+    pred print_m i:(map K V) o:string.
+    print_m (empty) "emtpy".
+    print_m (node L _ _ R H) S :-
+      print_m L SL,
+      print_m R SR,
+      S is "(" ^ SL ^ "," ^ (int_to_string H) ^ "," ^ SR ^ ")"
+      .
+
+    pred bal i:map K V, i:K, i:V, i:map K V, o:map K V.
+    bal L K V R T :-
+      height L HL,
+      height R HR,
+      HL2 is HL + 2,
+      HR2 is HR + 2,
+      bal.aux HL HR HL2 HR2 L K V R T.
+
+    pred bal.aux i:int, i:int, i:int, i:int, i:map K V, i:K, i:V, i:map K V, o:map K V.
+    bal.aux HL _ _ HR2 (node LL LV LD LR _) X D R T :-
+      HL > HR2, {height LL} >= {height LR}, !,
+      create LL LV LD {create LR X D R} T.
+    bal.aux HL _ _ HR2 (node LL LV LD (node LRL LRV LRD LRR _) _) X D R T :-
+      HL > HR2, !,
+      create {create LL LV LD LRL} LRV LRD {create LRR X D R} T.
+    bal.aux _ HR HL2 _ L X D (node RL RV RD RR _) T :-
+      HR > HL2, {height RR} >= {height RL}, !,
+      create {create L X D RL} RV RD RR T.
+    bal.aux _ HR HL2 _ L X D (node (node RLL RLV RLD RLR _) RV RD RR _) T :-
+      HR > HL2, !,
+      create {create L X D RLL} RLV RLD {create RLR RV RD RR} T.
+    bal.aux _ _ _ _ L K V R T :- create L K V R T.
+
+    pred add i:map K V, i:(pred i:K, i:K, o:cmp), i:K, i:V, o:map K V.
+    add empty _ K V T :- create empty K V empty T.
+    add (node _ X _ _ _ as M) Cmp X1 XD M1 :- Cmp X1 X E, !, add.aux E M Cmp X1 XD M1.
+
+    pred add.aux i:cmp, i:map K V, i:(pred i:K, i:K, o:cmp), i:K, i:V, o:map K V.
+    add.aux eq (node L _ _ R H) _   X XD T :- T = node L X XD R H, !.
+    add.aux lt (node L V D R _) Cmp X XD T :- bal {add L Cmp X XD} V D R T, !.
+    add.aux gt (node L V D R _) Cmp X XD T :- bal L V D {add R Cmp X XD} T, !.
+
+    pred update i:map K V, i:(pred i:K, i:K, o:cmp), i:K, i:V, o:map K V.
+    update (node _ X _ _ _ as M) Cmp X1 XD M1 :-
+      Cmp X1 X E, update.aux E M Cmp X1 XD M1.
+
+    pred update.aux i:cmp, i:map K V, i:(pred i:K, i:K, o:cmp), i:K, i:V, o:map K V.
+    update.aux eq (node L V _ R H) _   X XD (node L V XD R H).
+    update.aux lt (node L V D R H) Cmp X XD (node LT V D R H) :- update L Cmp X XD LT, !.
+    update.aux gt (node L V D R H) Cmp X XD (node L V D RT H) :- update R Cmp X XD RT, !.
+
+    pred find i:map K V, i:(pred i:K, i:K, o:cmp), i:K, o:V.
+    find ((node L K1 V1 R _) as M) Cmp K V :-
+      Cmp K K1 E, find.aux E Cmp L R V1 K V.
+
+    pred find.aux i:cmp, i:(pred i:K, i:K, o:cmp), i:map K V, i:map K V, i:V, i:K, o:V.
+    find.aux eq _   _ _ V _ V.
+    find.aux lt Cmp L _ _ K V :- find L Cmp K V.
+    find.aux gt Cmp _ R _ K V :- find R Cmp K V.
+
+    pred remove-min-binding i:map K V, o:map K V.
+    remove-min-binding (node empty _ _ R _) R :- !.
+    remove-min-binding (node L V D R _) X :- bal {remove-min-binding L} V D R X.
+
+    pred min-binding i:map K V, o:K, o:V.
+    min-binding (node empty V D _ _) V D :- !.
+    min-binding (node L _ _ _ _) V D :- min-binding L V D.
+
+    pred merge i:map K V, i:map K V, o:map K V.
+    merge empty X X :- !.
+    merge X empty X :- !.
+    merge M1 M2 R :-
+      min-binding M2 X D,
+      bal M1 X D {remove-min-binding M2} R.
+
+    pred remove i:map K V, i:(pred i:K, i:K, o:cmp), i:K, o:map K V.
+    remove empty _ _ empty :- !.
+    remove (node L V D R _) Cmp X M :- Cmp X V E, remove.aux E Cmp L R V D X M.
+
+    pred remove.aux i:cmp, i:(pred i:K, i:K, o:cmp), i:map K V, i:map K V, i:K, i:V, i:K, o:map K V.
+    remove.aux eq _   L R _ _ _ M :- merge L R M.
+    remove.aux lt Cmp L R V D X M :- bal {remove L Cmp X} V D R M.
+    remove.aux gt Cmp L R V D X M :- bal L V D {remove R Cmp X} M.
+
+    pred bindings i:map K V, i:list (pair K V), o:list (pair K V).
+    bindings empty X X.
+    bindings (node L V D R _) X X1 :-
+      bindings L [pr V D|{bindings R X}] X1.
+
+  } % std.map2.private
+} % std.map2
diff --git a/apps/tc-tabled/elpi/tabled_type_class.elpi b/apps/tc-tabled/elpi/tabled_type_class.elpi
new file mode 100644
index 000000000..ee3b5dc2d
--- /dev/null
+++ b/apps/tc-tabled/elpi/tabled_type_class.elpi
@@ -0,0 +1,426 @@
+/*
+(* https://github.com/leanprover/lean4/blob/cade21/src/Lean/Meta/SynthInstance.lean *)
+(* https://github.com/LPCIC/coq-elpi/blob/master/builtin-doc/coq-builtin.elpi *)
+(* Tabled type class : https://github.com/purefunctor/tabled-typeclass-resolution?tab=readme-ov-file *)
+(* https://github.com/purefunctor/tabled-typeclass-resolution/blob/main/src/lib.rs *)
+(* ty = https://github.com/leanprover/lean4/blob/cade21/src/Lean/Expr.lean#L152-L165 *)
+(* Coq-Stlc: https://lpcic.github.io/coq-elpi/stlc.txt *)
+(* https://github.com/leanprover/lean4/blob/master/src/Lean/Expr.lean#L302-L512 *)
+*/
+
+typeabbrev ty term.
+
+kind data type.
+type data ty -> list data -> data.
+
+kind assertion type.
+type assertion term -> term -> assertion.
+
+kind consumer_node type.
+type consumer_node assertion -> list assertion -> consumer_node.
+
+kind waiter type.
+type root waiter.
+type callback consumer_node -> waiter.
+
+kind entry type.
+type entry list waiter -> list assertion -> entry.
+
+typeabbrev resume_stack (list (pair consumer_node assertion)).
+
+% typeabbrev instance tc-instance.
+typeabbrev instance pair term term.
+
+kind generator_node type.
+type generator_node assertion -> list instance -> generator_node.
+
+kind synth type.
+type synth list generator_node ->
+  resume_stack ->
+  mymap assertion entry ->
+  option assertion ->
+  list (pair term term) ->
+  synth.
+
+pred type_equal i:ty i:ty o:cmp.
+type_equal X Y Cmp :-
+  ground_term X,
+  ground_term Y,
+  cmp_term X Y Cmp.
+type_equal X Y eq :- var X, var Y.
+type_equal (app L) (app G) Cmp :- type_equal_list L G Cmp.
+type_equal X Y lt :- var X, ground_term Y.
+type_equal X Y gt :- ground_term X, var Y.
+
+pred type_equal_list i:list ty i:list ty o:cmp.
+type_equal_list [ X | XS ] [ Y | YS ] Cmp :-
+    type_equal X Y eq,
+    type_equal_list XS YS Cmp.
+type_equal_list [ X | _ ] [ Y | _ ] Cmp :-
+    type_equal X Y Cmp,
+    not (Cmp = eq).
+type_equal_list [] [] eq.
+
+pred assertion_equal i:assertion i:assertion o:cmp.
+assertion_equal (assertion A _) (assertion B _) Cmp :-
+  type_equal A B Cmp,
+  !
+  /* Deterministic ! */
+  .
+
+pred term_typeclass i:term o:gref.
+term_typeclass (global Name) Name.
+term_typeclass (app [X | _]) N :- term_typeclass X N.
+term_typeclass (prod X T F) N :-
+  pi x\ term_typeclass (F x) N.
+
+pred assertion_typeclass i:assertion o:gref.
+assertion_typeclass (assertion G _) Name :- term_typeclass G Name.
+
+pred context_instances i:list (pair term term) i:gref o:list instance.
+context_instances [] _ [].
+context_instances [pr T V | XS] Name O :-
+  (if (term_typeclass T Name) (O = [ (pr T V) | OS ]) (O = OS)),
+  context_instances XS Name OS.
+
+pred tc_to_inst i:tc-instance o:instance.
+tc_to_inst (tc-instance BI _ as TcInst) (pr B BITm) :-
+  tc_instance_to_term TcInst B,
+  coq.env.global BI BITm.
+
+pred new_subgoal i:synth i:assertion i:waiter o:synth.
+new_subgoal
+  (synth GeneratorStack ResumeStack AssertionTable RootAnswer Ctx)
+  Subgoal Waiter
+  (synth NewGeneratorStack ResumeStack NewAssertionTable RootAnswer Ctx) :-
+  mymap_add Subgoal Entry AssertionTable NewAssertionTable,
+  Entry = (entry [Waiter] []),
+  assertion_typeclass Subgoal Name,
+  coq.TC.db-for Name TcInstances,
+  std.map TcInstances tc_to_inst Instances,
+  context_instances Ctx Name CtxInstances,
+  std.append CtxInstances Instances AllInstances,
+  NewGeneratorStack = [(generator_node Subgoal AllInstances) | GeneratorStack]
+  .
+
+/* Apply answer to goal and update meta variable context if it succeeds */
+
+pred replace_var_term i:ty o:ty i:ty o:ty.
+replace_var_term X Y (app L) (app G) :-
+  std.map L (replace_var_term X Y) G.
+replace_var_term X Y Z W :-
+  var Z,
+  X == Z,
+  W = Y
+  .
+replace_var_term X Y Z Z.
+
+pred replace_var_in_list i:ty o:ty i:list assertion o:list assertion.
+replace_var_in_list X Y [ assertion TA VA | AS ] [ assertion TB VB | BS ] :-
+    replace_var_term X Y TA TB,
+    replace_var_term X Y VA VB,
+    replace_var_in_list X Y AS BS.
+replace_var_in_list _ _ [] [].
+
+pred try_answer_type i:ty o:ty i:ty o:ty i:list assertion o:list assertion.
+try_answer_type X Y IX IY Lin Lout :-
+  var X, var Y,
+  replace_var_term X Y IX IY,
+  replace_var_in_list X Y Lin Lout.
+try_answer_type (app L) (app G) IX IY Lin Lout :-
+  try_answer_type_list L G IX IY Lin Lout.
+try_answer_type X Y IX IY Lin Lout :-
+  var X, ground_term Y, replace_var_term X Y IX IY, replace_var_in_list X Y Lin Lout.
+try_answer_type X Y I I L L :-
+  ground_term X,
+  ground_term Y,
+  cmp_term X Y eq.
+
+pred try_answer_type_list i:list ty o:list ty i:ty o:ty i:list assertion o:list assertion.
+try_answer_type_list [ X | XS ] [ Y | YS ] IX IY Lin Lout :-
+    try_answer_type X Y IX Itemp Lin Ltemp,
+    try_answer_type_list XS YS Itemp IY Ltemp Lout.
+try_answer_type_list [] [] I I L L.
+
+pred try_answer i:assertion o:assertion i:assertion o:assertion i:list assertion o:list assertion.
+try_answer (assertion A VA) (assertion B VB) (assertion G IA) (assertion G IB) Lin Lout :-
+  try_answer_type A B IA ITemp Lin Lout,
+  replace_var_term VA VB ITemp IB.
+
+pred replace_list i:list term i:term i:term o:list term.
+replace_list [ A | XS ] A B [ B | YS ] :-
+    !,
+    replace_list XS A B YS.
+replace_list [ C | XS ] A B [ C | YS ] :-
+    replace_list XS A B YS.
+replace_list [] _ _ [].
+
+pred extract_helper i:term i:int i:term o:term.
+extract_helper X Index (prod N T F) (prod N T G) :-
+  !,
+  pi x\
+    extract_helper X Index (F x) (G x).
+extract_helper X Index (app L) (app NewL) :-
+  !,
+  std.split-at Index L Lfront [ V | Ltail ],
+  replace_list L V X NewL.
+
+pred is_var_at_index i:term i:int.
+is_var_at_index (prod N T F) I :-
+  pi x\
+    is_var_at_index (F x) I.
+is_var_at_index (app L) I :-
+  std.split-at I L Lfront [ T | Ltail],
+  var T.
+
+pred extract_variables i:list term i:int o:term.
+  extract_variables L -1 (app L).
+extract_variables L Index Tm :-
+  PrevIndex is Index - 1,
+  extract_variables L PrevIndex PrevTm,
+  !,
+  ((is_var_at_index PrevTm Index,
+   Tm = prod TmX TmT TmF,
+   pi x\
+     extract_helper x Index PrevTm (TmF x)
+  );
+  (Tm = PrevTm))
+  .
+
+pred re_generalize i:list term o:list term.
+re_generalize [ X | Tl ] R :-
+  coq.typecheck X T ok,
+  (
+    (T = (app Tlist),
+     std.length Tlist Len,
+     Index is Len - 1,
+     extract_variables Tlist Index NewR,
+     R = [ NewR | RTl ]
+     );
+    (R = RTl)
+  ),
+  re_generalize Tl RTl
+  .
+re_generalize [ X | Tl ] [] :-
+  re_generalize Tl R.
+re_generalize [ ] [].
+
+pred tc_instance_to_term i:tc-instance o:term.
+tc_instance_to_term (tc-instance (const C) _) T :-
+  coq.env.const C _ /* Body */ Type,
+  coq.gref->string (const C) _ /* Name */,
+  T = Type.
+
+pred does_type_resolve i:term o:term.
+does_type_resolve X Y :-
+  var Y,
+  X = Y.
+does_type_resolve X Y :-
+  var X.
+does_type_resolve (app L) (app G) :-
+  std.map L does_type_resolve G.
+does_type_resolve X Y :-
+  ground_term X,
+  X = Y.
+
+pred try_resolve_types i:term i:term o:list term o:list assertion.
+try_resolve_types A (prod X T F) OL L :-
+  coq.typecheck V T ok,
+  try_resolve_types A (F V) OLS LS,
+  (OL = [ V | OLS]),
+  ((T = app _ ; L = [ assertion T V | LS ]) ; (L = LS)) /* TODO : better 'contains instance or var test' */
+    .
+try_resolve_types A B [] [] :-
+  does_type_resolve A B
+    .
+
+pred helper_fn i:term o:assertion.
+helper_fn A (assertion A V).
+
+pred simpl i:term o:term.
+simpl (app [ prod X T F , Arg | Tl ]) R :-
+  simpl (app [ (F Arg) | Tl ]) R.
+simpl (app [ A ]) A.
+simpl A A.
+
+pred filter_metavariables i:list assertion o:list assertion.
+filter_metavariables [ assertion (app L) V | XS ] [ assertion (app L) V | YS ] :-
+    !, filter_metavariables XS YS.
+filter_metavariables [ assertion X _ | XS ] YS :-
+    filter_metavariables XS YS.
+filter_metavariables [] [].
+
+
+pred try_resolve i:assertion i:instance o:assertion o:list assertion.
+try_resolve (assertion A _) (pr B BITm) (assertion RT RV) RL :-
+  % tc_instance_to_term (tc-instance BI _) B,
+  % coq.env.global BI BITm,
+  % coq.gref->string BI BIName,
+  % BI = const (BIConst),
+  % coq.env.const BIConst (some BIBody) BITy,
+  try_resolve_types A B OL L,
+  filter_metavariables L RL,
+    !,
+  RT = A,
+  ((OL = [], RV = BITm) ; RV = app [ BITm | OL ])
+    .
+
+pred temp_fun i:consumer_node i:assertion o:(pair consumer_node assertion).
+temp_fun A B (pr A B).
+
+pred waiter_fun i:assertion i:waiter i:(pair (resume_stack) (option assertion)) o:(pair (resume_stack) (option assertion)).
+waiter_fun Answer root (pr A _) (pr A (some Answer)).
+waiter_fun Answer (callback C) (pr A R) (pr [pr C Answer | A] R).
+
+pred new_consumer_node i:synth i:consumer_node o:synth.
+new_consumer_node
+    (synth GeneratorStack ResumeStack AssertionTable RootAnswer Ctx)
+    (consumer_node Goal [])
+    (synth GeneratorStack NewResumeStack NewAssertionTable NewRootAnswer Ctx) :-
+  /* for each solution to g, push new cnode onto resume stack with it */
+  mymap_find Goal AssertionTable (entry Waiters Answers),
+  /* for each solution to g, push new cnode onto resume stack with it */
+  std.fold Waiters (pr ResumeStack RootAnswer) (waiter_fun Goal) (pr NewResumeStack NewRootAnswer),
+  /* add new cnode to g's dependents */
+  mymap_update Goal NewEntry AssertionTable NewAssertionTable,
+  NewEntry = (entry Waiters [ Goal | Answers ]),
+  !.
+
+new_consumer_node
+    (synth GeneratorStack ResumeStack AssertionTable RootAnswer Ctx)
+    (consumer_node _ [ Subgoal | _ ] as CN)
+    (synth NewGeneratorStack NewResumeStack NewAssertionTable RootAnswer Ctx) :-
+  if (mymap_find Subgoal AssertionTable (entry Waiters Answers))
+     (
+       /* Map answers with consumer node */
+       /* Add cnode onto G's dependents? */
+       std.map Answers (temp_fun CN) TempResumeStack,
+       std.append TempResumeStack ResumeStack NewResumeStack,
+
+       NewWaiters = [ callback CN | Waiters ],
+       mymap_update Subgoal NewEntry AssertionTable NewAssertionTable,
+       NewEntry = (entry NewWaiters Answers),
+       NewGeneratorStack = GeneratorStack
+     )
+     (
+       new_subgoal
+         (synth GeneratorStack ResumeStack AssertionTable RootAnswer Ctx)
+         Subgoal
+         (callback CN)
+         (synth NewGeneratorStack NewResumeStack NewAssertionTable RootAnswer Ctx)
+     ),
+     !.
+
+new_consumer_node _ _ _ :- coq.error "Failed new consumer node!" , fail.
+
+pred tabled_typeclass_resolution_body i:synth i:assertion o:synth o:assertion.
+tabled_typeclass_resolution_body (synth _ _ _ (some Answer) _) _ _ Answer.
+
+tabled_typeclass_resolution_body (synth GeneratorStack
+				  [ (pr (consumer_node Goal [ Subgoal | Remaining ]) Answer) | ResumeStack ]
+				  AssertionTable RootAnswer Ctx)
+    Query MySynth FinalAnswer :-
+  Answer = assertion AnswerT AnswerV,
+  coq.typecheck AnswerV AnswerNT ok,
+  NewAnswer = assertion AnswerNT AnswerV,
+  if (try_answer Subgoal NewAnswer Goal UpdatedGoal Remaining UpdatedRemaining)
+     (
+       new_consumer_node
+         (synth GeneratorStack ResumeStack AssertionTable RootAnswer Ctx)
+         (consumer_node UpdatedGoal UpdatedRemaining) /* TODO: Was Goal in code, but should add new solution? */
+         MySynth
+      )
+      (
+        MySynth = (synth GeneratorStack ResumeStack AssertionTable RootAnswer Ctx)
+      ).
+
+tabled_typeclass_resolution_body (synth GeneratorStack
+				  [ (pr (consumer_node Goal []) Answer) | ResumeStack ]
+				  AssertionTable RootAnswer Ctx)
+    Query MySynth FinalAnswer :-
+  coq.warn "Cannot resume with empty subgoals!",
+  fail.
+
+tabled_typeclass_resolution_body
+  (synth [ generator_node Goal [Instance | Instances ] | GeneratorStack ]
+    ResumeStack AssertionTable RootAnswer Ctx) Query NewSynth FinalAnswer :-
+  if (try_resolve Goal Instance Resolved Subgoals)
+     (
+       /* else (l. 14) */
+       new_consumer_node
+         (synth [ generator_node Goal Instances | GeneratorStack ] ResumeStack AssertionTable RootAnswer Ctx)
+         (consumer_node Resolved Subgoals) NewSynth
+     )
+     (
+       /* If first subgoal of cnode does not resolve with solution then Continue */
+       NewSynth = (synth [ generator_node Goal Instances | GeneratorStack ] ResumeStack AssertionTable RootAnswer Ctx)
+     ).
+
+tabled_typeclass_resolution_body (synth
+				  [ generator_node _ [] | GeneratorStack ]
+				  ResumeStack AssertionTable RootAnswer Ctx)
+    Query
+    (synth GeneratorStack ResumeStack AssertionTable RootAnswer Ctx) FinalAnswer.
+/* If cnode has no remaining subgoals then (ll.7-13) .. */
+
+tabled_typeclass_resolution_body (synth [] [] _ _ Ctx) _ _ _ :-
+  coq.warn "Failed to find instance: Nothing left to test",
+  fail.
+
+pred synth_loop i:synth i:assertion i:int o:assertion.
+synth_loop (synth _ _ _ (some Answer) _) _ Fuel Answer :- coq.say "synth round" Fuel.
+synth_loop MySynth Query Fuel FinalAnswer :-
+  Fuel > 0,
+  tabled_typeclass_resolution_body MySynth Query NextSynth FinalAnswer,
+  !,
+  NextFuel is Fuel - 1,
+  synth_loop NextSynth Query NextFuel FinalAnswer.
+
+pred tabled_typeclass_resolution i:list (pair term term) i:assertion o:assertion.
+tabled_typeclass_resolution Ctx Query FinalAnswer :-
+  mymap_make assertion_equal AssertionTableEmpty,
+  new_subgoal (synth [] [] AssertionTableEmpty none Ctx) Query root MySynth,
+  /* while true do */
+  synth_loop MySynth Query 20000 FinalAnswer,
+  !.
+
+pred context_to_arg_pairs i:list goal-ctx o:list (pair term term).
+context_to_arg_pairs [] [].
+context_to_arg_pairs [ decl V _ T | XS ] [ pr T V | YS ] :-
+  !, context_to_arg_pairs XS YS.
+context_to_arg_pairs [ _ | XS ] YS :-
+  context_to_arg_pairs XS YS.
+
+pred args_to_arg_pairs i:list argument o:list (pair term term).
+args_to_arg_pairs [] [].
+args_to_arg_pairs [ ctx-decl (context-item _ _ _ _ _ as CtxI) | XS ] [ pr T V | YS ] :-
+  !,
+  args_to_arg_pairs XS YS.
+args_to_arg_pairs [ _ | XS ] YS :-
+  args_to_arg_pairs XS YS.
+
+pred tabled_proof_search i:list goal-ctx i:list argument i:term o:term.
+tabled_proof_search Ctx Args Type PRoof :-
+  MyGoal = assertion Type {{ _ }},
+  context_to_arg_pairs Ctx CtxPairs,
+  args_to_arg_pairs Args ArgsPairs,
+  std.append CtxPairs ArgsPairs CtxInstances,
+  tabled_typeclass_resolution CtxInstances MyGoal FinalAnswer,
+  !,
+  /* Convert from result to proof term! */
+  FinalAnswer = assertion FinalType FinalTerm,
+  FinalProof = FinalTerm,
+  PRoof = FinalProof
+  .
+
+pred search_context i:list prop i:term o:term.
+search_context [decl Te _ Ty | _] Type PRoof :-
+  Ty = Type,
+  Te = PRoof.
+search_context [_|Tl] Type PRoof :-
+  search_context Tl Type PRoof.
+
+solve (goal Ctx Trigger Type PRoof Args as G) V :-
+  (search_context Ctx Type PRoof ; tabled_proof_search Ctx Args Type PRoof).
+
+solve _ _ :- coq.ltac.fail _ "No auto".
diff --git a/apps/tc-tabled/src/dune b/apps/tc-tabled/src/dune
new file mode 100644
index 000000000..e20e01ede
--- /dev/null
+++ b/apps/tc-tabled/src/dune
@@ -0,0 +1,11 @@
+; generated by make, do not edit
+
+(library
+ (name elpi_tc_tabled_plugin)
+ (public_name rocq-elpi.tc-tabled)
+ (flags :standard -w -27)
+ (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")"))
+ (libraries rocq-runtime.plugins.ltac rocq-runtime.vernac rocq-elpi.elpi))
+
+(coq.pp
+ (modules rocq_elpi_tc_tabled_hook))
diff --git a/apps/tc-tabled/src/dune.in b/apps/tc-tabled/src/dune.in
new file mode 100644
index 000000000..2b368d3a9
--- /dev/null
+++ b/apps/tc-tabled/src/dune.in
@@ -0,0 +1,9 @@
+(library
+ (name elpi_tc_tabled_plugin)
+ (public_name rocq-elpi.tc-tabled)
+ (flags :standard -w -27)
+ (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")"))
+ (libraries @@ROCQ_RUNTIME@@.plugins.ltac @@ROCQ_RUNTIME@@.vernac rocq-elpi.elpi))
+
+(coq.pp
+ (modules rocq_elpi_tc_tabled_hook))
diff --git a/apps/tc-tabled/src/rocq_elpi_tc_tabled_hook.mlg b/apps/tc-tabled/src/rocq_elpi_tc_tabled_hook.mlg
new file mode 100644
index 000000000..b3a681efd
--- /dev/null
+++ b/apps/tc-tabled/src/rocq_elpi_tc_tabled_hook.mlg
@@ -0,0 +1,9 @@
+(* license: GNU Lesser General Public License Version 2.1 or later           *)
+(* ------------------------------------------------------------------------- *)
+
+DECLARE PLUGIN "rocq-elpi.tc-tabled"
+
+{
+open Stdarg
+open Elpi_plugin
+}
diff --git a/apps/tc-tabled/tests/diamond.v b/apps/tc-tabled/tests/diamond.v
new file mode 100644
index 000000000..7b1c5d617
--- /dev/null
+++ b/apps/tc-tabled/tests/diamond.v
@@ -0,0 +1,181 @@
+(* https://github.com/leanprover/lean4/blob/master/tests/lean/run/typeclass_diamond.lean *)
+
+(* Diamond *)
+Class Top1   (n : nat) : Type.
+Class Bot1   (n : nat) : Type.
+Class Left1  (n : nat) : Type.
+Class Right1 (n : nat) : Type.
+
+Instance Bot1Inst : Bot1 0 := {}.
+Instance Left1ToBot1   (n : nat) `{Left1 n}  : Bot1 n := {}.
+
+Instance Right1ToBot1  (n : nat) `{Right1 n} : Bot1 n := {}.
+Instance Top1ToLeft1   (n : nat) `{Top1 n}   : Left1 n := {}.
+Instance Top1ToRight1  (n : nat) `{Top1 n}   : Right1 n := {}.
+Instance Bot1ToTopSucc (n : nat) `{Bot1 n}   : Top1 (S n) := {}.
+
+Class Top2 (n : nat) : Type.
+Class Bot2   (n : nat) : Type.
+Class Left2  (n : nat) : Type.
+Class Right2 (n : nat) : Type.
+
+Instance Left2ToBot2   (n : nat) `{Left2 n}  : Bot2 n := {}.
+Instance Right2ToBot2  (n : nat) `{Right2 n} : Bot2 n := {}.
+Instance Top2ToLeft2   (n : nat) `{Top2 n}   : Left2 n := {}.
+Instance Top2ToRight2  (n : nat) `{Top2 n}   : Right2 n := {}.
+Instance Bot2ToTopSucc (n : nat) `{Bot2 n}   : Top2 (S n) := {}.
+
+Class Top (n : nat) : Type.
+
+Instance Top1ToTop (n : nat) `{Top1 n} : Top n := {}.
+Instance Top2ToTop (n : nat) `{Top2 n} : Top n := {}.
+
+(* (* Finished transaction in 0.001 secs (0.001u,0.s) (successful) *) *)
+(* Module Top4Rocq. Time Instance Top4 : Top 4 := _. End Top4Rocq. *)
+
+(* (* Finished transaction in 0.021 secs (0.021u,0.s) (successful) *) *)
+(* Module Top8Rocq. Time Instance Top8 : Top 8 := _. End Top8Rocq. *)
+
+(* (* Finished transaction in 4.661 secs (4.661u,0.s) (successful) *) *)
+(* Module Top16Rocq. Time Instance Top16 : Top 16 := _. End Top16Rocq. *)
+
+(* (* Finished transaction in 0.719 secs (0.717u,0.s) (successful) *) *)
+(* Module Top17Rocq. Time Instance Top17 : Top 17 := _. End Top17Rocq. *)
+
+(* (* Finished transaction in 1.409 secs (1.407u,0.s) (successful) *) *)
+(* Module Top18Rocq. Time Instance Top18 : Top 18 := _. End Top18Rocq. *)
+
+(* (* Finished transaction in 2.789 secs (2.785u,0.002s) (successful) *) *)
+(* Module Top19Rocq. Time Instance Top19 : Top 19 := _. End Top19Rocq. *)
+
+(* (* Finished transaction in 5.602 secs (5.597u,0.001s) (successful) *) *)
+(* Module Top20Rocq. Time Instance Top20 : Top 20 := _. End Top20Rocq. *)
+
+(* (* Finished transaction in 170.346 secs (170.255u,0.004s) (successful) *) *)
+(* Module Top21Rocq. Time Instance Top21 : Top 21 := _. End Top21Rocq. *)
+
+(* (* Finished transaction in 351.702 secs (351.432u,0.033s) (successful) *) *)
+(* Module Top22Rocq. Time Instance Top22 : Top 22 := _. End Top22Rocq. *)
+
+(* (* Finished transaction in 699.508 secs (699.034u,0.059s) (successful) *) *)
+(* Module Top23Rocq. Time Instance Top23 : Top 23 := _. End Top23Rocq. *)
+
+From elpi Require Import elpi.
+From elpi.apps Require Import tc.
+
+Elpi TC Solver Activate TC.Solver.
+Elpi TC Solver Override TC.Solver All.
+
+TC.AddAllClasses.
+TC.AddAllInstances.
+
+(* ELPI TC solver *)
+
+(* (* Finished transaction in 0.029 secs (0.029u,0.s) (successful) *) *)
+(* Module Top4ELPI_TC. Time Instance Top4 : Top 4 := _. End Top4ELPI_TC. *)
+
+(* (* Finished transaction in 0.035 secs (0.035u,0.s) (successful) *) *)
+(* Module Top8ELPI_TC. Time Instance Top8 : Top 8 := _. End Top8ELPI_TC. *)
+
+(* (* Finished transaction in 0.368 secs (0.367u,0.s) (successful) *) *)
+(* Module Top16ELPI_TC. Time Instance Top16 : Top 16 := _. End Top16ELPI_TC. *)
+
+(* (* Finished transaction in 0.719 secs (0.717u,0.s) (successful) *) *)
+(* Module Top17ELPI_TC. Time Instance Top17 : Top 17 := _. End Top17ELPI_TC. *)
+
+(* (* Finished transaction in 1.409 secs (1.407u,0.s) (successful) *) *)
+(* Module Top18ELPI_TC. Time Instance Top18 : Top 18 := _. End Top18ELPI_TC. *)
+
+(* (* Finished transaction in 2.789 secs (2.785u,0.002s) (successful) *) *)
+(* Module Top19ELPI_TC. Time Instance Top19 : Top 19 := _. End Top19ELPI_TC. *)
+
+(* (* Finished transaction in 5.602 secs (5.597u,0.001s) (successful) *) *)
+(* Module Top20ELPI_TC. Time Instance Top20 : Top 20 := _. End Top20ELPI_TC. *)
+
+(* (* Finished transaction in 12.295 secs (12.281u,0.002s) (successful) *) *)
+(* Module Top21ELPI_TC. Time Instance Top21 : Top 21 := _. End Top21ELPI_TC. *)
+
+(* (* Finished transaction in 27.964 secs (27.951u,0.003s) (successful) *) *)
+(* Module Top22ELPI_TC. Time Instance Top22 : Top 22 := _. End Top22ELPI_TC. *)
+
+(* (* Finished transaction in 49.262 secs (49.231u,0.008s) (successful) *) *)
+(* Module Top23ELPI_TC. Time Instance Top23 : Top 23 := _. End Top23ELPI_TC. *)
+
+(* (* Finished transaction in 101.836 secs (101.792u,0.017s) (successful) *) *)
+(* Module Top24ELPI_TC. Time Instance Top24 : Top 24 := _. End Top24ELPI_TC. *)
+
+(* (* Finished transaction in 205.469 secs (205.309u,0.032s) (successful) *) *)
+(* Module Top25ELPI_TC. Time Instance Top25 : Top 25 := _. End Top25ELPI_TC. *)
+
+
+(* / ELPI TC solver *)
+
+Elpi TC Solver Override TC.Solver None.
+
+From elpi.apps.tc_tabled Require Import tabled_type_class.
+
+(* Diamond example in Rocq *)
+Elpi TC Solver Activate TC.TabledSolver.
+Elpi TC Solver Override TC.TabledSolver All.
+
+(* Tabled solver *)
+
+(* Finished transaction in 0.023 secs (0.023u,0.s) (successful) *)
+Module Top4Tabled. Time Instance Top4 : Top 4 := _. End Top4Tabled.
+
+(* Finished transaction in 0.054 secs (0.054u,0.s) (successful) *)
+Module Top8Tabled. Time Instance Top8 : Top 8 := _. End Top8Tabled.
+
+(* Finished transaction in 0.201 secs (0.197u,0.003s) (successful) *)
+Module Top16Tabled. Time Instance Top16 : Top 16 := _. End Top16Tabled.
+
+(* Finished transaction in 0.273 secs (0.267u,0.005s) (successful) *)
+Module Top17Tabled. Time Instance Top17 : Top 17 := _. End Top17Tabled.
+
+(* Finished transaction in 0.255 secs (0.253u,0.s) (successful) *)
+Module Top18Tabled. Time Instance Top18 : Top 18 := _. End Top18Tabled.
+
+(* Finished transaction in 0.289 secs (0.286u,0.001s) (successful) *)
+Module Top19Tabled. Time Instance Top19 : Top 19 := _. End Top19Tabled.
+
+(* Finished transaction in 0.369 secs (0.36u,0.007s) (successful) *)
+Module Top20Tabled. Time Instance Top20 : Top 20 := _. End Top20Tabled.
+
+(* Finished transaction in 0.363 secs (0.351u,0.011s) (successful) *)
+Module Top21Tabled. Time Instance Top21 : Top 21 := _. End Top21Tabled.
+
+(* Finished transaction in 0.372 secs (0.372u,0.s) (successful) *)
+Module Top22Tabled. Time Instance Top22 : Top 22 := _. End Top22Tabled.
+
+(* Finished transaction in 0.419 secs (0.415u,0.003s) (successful) *)
+Module Top23Tabled. Time Instance Top23 : Top 23 := _. End Top23Tabled.
+
+(* Finished transaction in 0.507 secs (0.506u,0.s) (successful) *)
+Module Top24Tabled. Time Instance Top24 : Top 24 := _. End Top24Tabled.
+
+(* Finished transaction in 0.525 secs (0.519u,0.005s) (successful) *)
+Module Top25Tabled. Time Instance Top25 : Top 25 := _. End Top25Tabled.
+
+(* Finished transaction in 3.148 secs (3.147u,0.s) (successful) *)
+Module Top50Tabled. Time Instance Top50 : Top 50 := _. End Top50Tabled.
+
+(* Finished transaction in 10.138 secs (10.041u,0.092s) (successful) *)
+Module Top75Tabled. Time Instance Top75 : Top 75 := _. End Top75Tabled.
+
+(* Finished transaction in 26.328 secs (26.289u,0.006s) (successful) *)
+Module Top100Tabled. Time Instance Top100 : Top 100 := _. End Top100Tabled.
+
+(* Finished transaction in 48.959 secs (48.772u,0.174s) (successful) *)
+Module Top125Tabled. Time Instance Top125 : Top 125 := _. End Top125Tabled.
+
+(* Finished transaction in 87.289 secs (87.152u,0.13s) (successful) *)
+Module Top150Tabled. Time Instance Top150 : Top 150 := _. End Top150Tabled.
+
+(* Finished transaction in 152.848 secs (152.537u,0.223s) (successful) *)
+Module Top175Tabled. Time Instance Top175 : Top 175 := _. End Top175Tabled.
+
+(* Finished transaction in 247.147 secs (246.117u,0.948s) (successful) *)
+Module Top200Tabled. Time Instance Top200 : Top 200 := _. End Top200Tabled.
+
+(* / Tabled solver *)
+(* Finished transaction in 726.238 secs (725.633u,0.254s) (successful) *)
diff --git a/apps/tc-tabled/tests/dune b/apps/tc-tabled/tests/dune
new file mode 100644
index 000000000..89a9b7f79
--- /dev/null
+++ b/apps/tc-tabled/tests/dune
@@ -0,0 +1,8 @@
+(coq.theory
+ (name elpi.apps.tc_tabled.tests)
+ (flags :standard -async-proofs-cache force)
+ (package rocq-elpi-tests)
+ (theories elpi elpi.apps.tc elpi.apps.tc_tabled))
+
+(include_subdirs qualified)
+(dirs :standard \ WIP)
diff --git a/apps/tc-tabled/theories/dune b/apps/tc-tabled/theories/dune
new file mode 100644
index 000000000..0982f7a46
--- /dev/null
+++ b/apps/tc-tabled/theories/dune
@@ -0,0 +1,8 @@
+(coq.theory
+ (name elpi.apps.tc_tabled)
+ (package rocq-elpi)
+ (theories elpi elpi.apps.tc elpi.apps.tc_tabled.elpi)
+ (flags -w -all -w -elpi)
+ (plugins rocq-elpi.tc-tabled))
+
+(include_subdirs qualified)
diff --git a/apps/tc-tabled/theories/tabled_type_class.v b/apps/tc-tabled/theories/tabled_type_class.v
new file mode 100644
index 000000000..5bb1f2042
--- /dev/null
+++ b/apps/tc-tabled/theories/tabled_type_class.v
@@ -0,0 +1,50 @@
+From elpi Require Import elpi.
+From elpi.apps Require Import tc.
+
+Elpi Tactic TC.TabledSolver.
+Elpi TC Solver Register TC.TabledSolver.
+
+Declare ML Module "rocq-elpi.tc-tabled".
+
+From elpi.apps.tc_tabled.elpi Extra Dependency "custom_map.elpi" as custom_map.
+From elpi.apps.tc_tabled.elpi Extra Dependency "map2.elpi" as map2.
+From elpi.apps.tc_tabled.elpi Extra Dependency "tabled_type_class.elpi" as TabledTC.
+
+Elpi Accumulate File custom_map.
+Elpi Accumulate File map2.
+
+Elpi Accumulate lp:{{
+  pred mymap_make i:(pred i:K, i:K, o:cmp), o:mymap K V.
+  pred mymap_find i:K i:(mymap K V) o:V.
+  pred mymap_add i:K i:V i:(mymap K V) o:(mymap K V).
+  pred mymap_update i:K i:V i:(mymap K V) o:(mymap K V).
+
+  /*
+  typeabbrev (mymap K V) (custom_map K V).
+
+  mymap_make Cmp M :- custom_make Cmp M.
+  mymap_find K M V :- custom_find K M V.
+  mymap_add K V M M1 :- custom_add K V M M1.
+  mymap_update K V M M1 :- custom_add K V M M1.
+  */
+
+  typeabbrev (mymap K V) (std.map2 K V).
+
+  mymap_make Cmp M :- std.map2.make Cmp M.
+  mymap_find K M V :- std.map2.find K M V.
+  mymap_add K V M M1 :- std.map2.add K V M M1.
+  mymap_update K V M M1 :- std.map2.update K V M M1.
+
+  /*
+  typeabbrev (mymap K V) (avl.tree K V).
+
+  mymap_make Cmp M :- avl.empty Cmp M.
+  mymap_find K M V :- avl.lookup_node K M V.
+  mymap_add K V M M1 :- avl.insert_node K V M M1.
+  mymap_update K V M M1 :- avl.update_node K V M M1.
+  */
+}}.
+
+Elpi Accumulate File TabledTC.
+
+Elpi Export TC.TabledSolver.