diff --git a/derive/derive.elpi b/derive/derive.elpi
index 86d6eb7f0..53a40e58b 100644
--- a/derive/derive.elpi
+++ b/derive/derive.elpi
@@ -47,7 +47,7 @@ main T M :-
     derive.bcongr.main T {calc (Indname ^ "bcongr_")},
     derive.eqK.main T {calc (Indname ^ "eq_axiom_")},
     derive.eqcorrect.main T {calc (Indname ^ "eq_correct")},
-    simplify (eqcorrect-db T) {calc (Indname ^ "eq_OK")}
+    derive.eqOK T {calc (Indname ^ "eq_OK")}
   ].
   
 }
diff --git a/derive/eqOK.elpi b/derive/eqOK.elpi
index f4ee9d561..58da7ff60 100644
--- a/derive/eqOK.elpi
+++ b/derive/eqOK.elpi
@@ -4,68 +4,38 @@
 
 namespace derive.eqOK {
 
-strip-last-arg (app [Hd|Args]) X R :-
-  appendR Prefix [X] Args,
-  if (Prefix = []) (R = Hd) (R = app[Hd|Prefix]).
+pred body i:int, i:term, i:term, i:term, o:term.
+
+body N (prod NA A a\ prod NF (A_eq a) (B a)) E P
+       (lam NA A a\ lam NF (A_eq a) f\
+         lam `p` (PA a f) (B1 a f)) :-
+  N > 0, !, M is N - 1,
+  @pi-decl NA A a\
+  @pi-decl NF (A_eq a) f\
+    (PA a f = {{ forall x : lp:a, @elpi.derive.eqK.eq_axiom lp:a lp:f x }},
+     @pi-decl `p` (PA a f) p\
+       body M (B a f) {mk-app E [a,f]}
+                      {mk-app P [a, {{@elpi.derive.eqK.eq_axiom lp:a lp:f}}, p]}
+          (B1 a f p)).
 
-trivial? T P :-
-  strip-last-arg T X Pred,
-  prove Pred Proof, mk-app Proof [X] P.
-
-prove X _ :- coq.say "prove" X, fail.
-prove X P :- param1P-db X P.
-prove (app[X|Args]) (app[P|PArgs]) :-
-  param1P-db X P,
-  prove-args Args PArgs.
-
-prove-args [] [].
-prove-args [X,PX|Args] [X,PX,QX|PArgs] :-
-  prove PX QX,
-  prove-args Args PArgs.
-
-hyp (prod _ S T) T1 H Args (lam `_` S _\ R) :-
-  /*safe-dest-app S HD ArgsS, appendR As [_] ArgsS,
-  constant? HD As, !,
-  pi x\ hyp (T x) T1 H Args R.*/ trivial? S P, !,
-  hyp (T P) T1 H Args R.
-
-hyp (prod N S T) (prod N S T1) H Args (lam N S R) :- !,
-  pi x\ hyp (T x) (T1 x) H [x|Args] (R x).
-
-hyp T T H A R :- mk-app H {rev A} R.
-
-% Looks like a property on the parameter: specialize
-body (prod N (sort _ as S) x\
-       prod _ (prod _ x _\ sort _) px\ T x px) B Args (lam N S R) :- !,
-  pi x\ sigma A\
-    A = {{ @elpi.derive.param1.UnitPred lp:x }},
-    decl x N S =>
-      body (T x A) B [A,x|Args]  (R x).
+% done
+body 0 (prod N S x\ prod _ _ _) E P (lam N S R) :-
+  @pi-decl N S x\ mk-app E [x,{mk-app P [x]}] (R x).
 
-% A trivial premise: prove
-body (prod _ S T) B Args R :- trivial? S P, !,
-  body (T P) B [P|Args] R.
+main T O [] :- 
+  assert (T = indt GR) "derive.eqOK: not an inductive type",
+  coq.env.indt GR _ Lno _ _ _ _,
 
-% A regular premise: recursively simplify
-body (prod N S T) B Args (lam N TX R) :- !,
-  @pi-decl N S x\
-    (hyp S TX x [] (A x), body (T x) B [A x|Args] (R x)).
+  assert (eqcorrect-db T E) "derive.eqOK: use derive.eqcorrect before",
+  coq.env.typeof-gr {term->gr E} ETy,
 
-% done
-body _ B Args R :- mk-app B {rev Args} R.
+  assert (reali T IsT) "derive.eqOK: use derive.param1 before",
+  assert (param1P-db IsT TisT) "derive.eqOK: use derive.param1P before",
 
-log P :- P, !.
-log _ :- coq.say "type checking fails", fail.
+  body Lno ETy E TisT NewBo,
+coq.say {coq.term->string NewBo},
+  coq.typecheck NewBo NewTy,
 
-main T O [] :- do! [
-  coq.env.typeof-gr {term->gr T} Ty,
-  body Ty T [] NewBo,
-  coq.say {coq.term->string NewBo},
-  log (coq.typecheck NewBo NewTy),
-  % TODO: also fix eta expansions
-  (pi F X T\ copy (app [lam _ _ F, X]) T :- !, copy (F X) T) =>
-     copy NewTy NewTyNice,
-  coq.env.add-const O NewBo NewTyNice @opaque! _
-].
+  coq.env.add-const O NewBo NewTy @opaque! _.
 
 }
diff --git a/theories/derive/eqOK.v b/theories/derive/eqOK.v
index dce454992..054b0d0d6 100644
--- a/theories/derive/eqOK.v
+++ b/theories/derive/eqOK.v
@@ -3,15 +3,15 @@
    license: GNU Lesser General Public License Version 2.1 or later           
    ------------------------------------------------------------------------- *)
 
-From elpi Require Import elpi derive.param1 derive.param1P.
+From elpi Require Import elpi derive.param1 derive.param1P derive.eqK derive.eqcorrect.
 
 Elpi Command derive.eqOK.
 
 Elpi Accumulate File "coq-lib-extra.elpi".
 Elpi Accumulate File "derive/param1.elpi".
 Elpi Accumulate Db derive.param1.db.
-
 Elpi Accumulate Db derive.param1P.db.
+Elpi Accumulate Db derive.eqcorrect.db.
 
 Elpi Accumulate File "derive/eqOK.elpi".
 Elpi Accumulate "
@@ -22,7 +22,7 @@ Elpi Accumulate "
   main _ :- usage.
 
   usage :-
-    coq.error ""Usage: derive.eqOK <term name> [<output name>]"".
+    coq.error ""Usage: derive.eqOK <inductive name> [<output name>]"".
 ".  
 Elpi Typecheck.
 
diff --git a/theories/derive/param1P.v b/theories/derive/param1P.v
index e96468c0f..28aa1f6a7 100644
--- a/theories/derive/param1P.v
+++ b/theories/derive/param1P.v
@@ -40,7 +40,7 @@ Elpi Accumulate "
     coq.locate I T,
     coq.gr->id {term->gr T} Tname,
     Name is Tname ^ ""_"",
-    derive.param1P.main T Name _.
+    derive.param1P.main T {rex_replace ""^is_"" """" Name} _.
   main _ :- usage.
 
   usage :-
diff --git a/theories/derive/tests/test_eqOK.v b/theories/derive/tests/test_eqOK.v
index 05c348824..20810a274 100644
--- a/theories/derive/tests/test_eqOK.v
+++ b/theories/derive/tests/test_eqOK.v
@@ -11,10 +11,7 @@ Elpi derive.eq nat.
 Elpi derive.eqK nat.
 Elpi derive.eqcorrect nat.
  
-Elpi derive.eqOK nat_induction nat_ind.
-Check nat_ind : forall P, P 0 -> (forall x, P x -> P (S x)) -> forall n, P n.
- 
-Elpi derive.eqOK nat_eq_correct nat_eqOK.
+Elpi derive.eqOK nat nat_eqOK.
 Check nat_eqOK : forall n, eq_axiom nat nat_eq n.
 
 Elpi derive.param1 list.
@@ -28,16 +25,11 @@ Elpi derive.eq list.
 Elpi derive.eqK list.
 Elpi derive.eqcorrect list.
 
-
-Elpi derive.eqOK list_induction list_ind.
-Check list_ind :
-  forall (A : Type) (P : list A -> Type),
-    P nil ->
-    (forall H : A, forall H0 : list A, P H0 -> P (H :: H0)%list) -> forall x : list A, P x.
-
-Elpi derive.eqOK list_eq_correct list_eqOK.
+Elpi derive.eqOK list list_eqOK.
 Check list_eqOK :
-  forall (A : Type) (F : A -> A -> bool) x, is_list A (eq_axiom A F) x -> eq_axiom (list A) (list_eq A F) x.
+  forall (A : Type) (F : A -> A -> bool)
+    (H : forall l, eq_axiom A F l) x,
+      eq_axiom (list A) (list_eq A F) x.
 
 Inductive dlist A := dnil | dcons (a : A * nat) (l : dlist A).
 
@@ -63,23 +55,9 @@ Elpi derive.eq dlist.
 Elpi derive.eqK dlist. 
 Elpi derive.eqcorrect dlist.
 
-Elpi derive.eqOK dlist_induction dlist_ind2.
-
-Check dlist_induction :
-  forall (A : Type) (PA : A -> Type) (P : dlist A -> Type),
-  P (dnil A) ->
-  (forall a : A * nat,
-   is_prod A PA nat is_nat a ->
-   forall l : dlist A, P l -> P (dcons A a l)) -> forall x : dlist A, is_dlist A PA x -> P x.
-
-Check dlist_ind2 :
-   forall (A : Type) (P : dlist A -> Type),
-       P (dnil A) ->
-       (forall a : A * nat, forall l : dlist A, P l -> P (dcons A a l)) ->
-       forall x : dlist A, P x.
-
-Elpi derive.eqOK dlist_eq_correct dlist_eqOK.
+Elpi derive.eqOK dlist dlist_eqOK.
 
 Check dlist_eqOK : 
-  forall A f l, is_dlist A (eq_axiom A f) l -> eq_axiom (dlist A) (dlist_eq A f) l.
+  forall A f (h : forall l, eq_axiom A f l) l,
+    eq_axiom (dlist A) (dlist_eq A f) l.
 
diff --git a/theories/derive/tests/test_param1P.v b/theories/derive/tests/test_param1P.v
index 47efbe70b..da3782372 100644
--- a/theories/derive/tests/test_param1P.v
+++ b/theories/derive/tests/test_param1P.v
@@ -3,13 +3,13 @@ From elpi Require Import derive.param1 derive.param1P.
 Elpi derive.param1 list.
 Elpi derive.param1P is_list.
 
-Check is_list_is_list :
+Check list_is_list :
   forall A P, (forall x : A, P x) -> forall l, is_list A P l.
 
 Elpi derive.param1 prod.
 Elpi derive.param1P is_prod.
 
-Check is_prod_is_prod :
+Check prod_is_prod :
   forall A P, (forall x : A, P x) -> 
   forall B Q, (forall x : B, Q x) -> 
     forall p, is_prod A P B Q p.
@@ -20,4 +20,4 @@ Elpi derive.param1 xx.
 Elpi derive.param1P is_xx.
 
 Check is_xx : xx -> Type.
-Check is_xx_is_xx : forall x : xx, is_xx x.
\ No newline at end of file
+Check xx_is_xx : forall x : xx, is_xx x.
\ No newline at end of file