diff --git a/elpi/param-class.elpi b/elpi/param-class.elpi
index 9c6f13c..26e8818 100644
--- a/elpi/param-class.elpi
+++ b/elpi/param-class.elpi
@@ -23,36 +23,47 @@ type map2b map-class.
 type map3  map-class.
 type map4  map-class.
 
+kind class-kind type.
+type low class-kind.
+type high class-kind.
+type all class-kind.
+
+pred map-classes o:class-kind, o:list map-class.
+map-classes all [map0, map1, map2a, map2b, map3, map4].
+map-classes low [map0, map1, map2a].
+map-classes high [map2b, map3, map4].
+
+pred sym-rel o:gref.
+sym-rel {{:gref lib:trocq.sym_rel}}.
+
+pred paths o:gref.
+paths {{:gref lib:trocq.paths}}.
+
 kind param-class type.
 type pc map-class -> map-class -> param-class.
 
+pred map->class o:map-class, o:gref.
+map->class map0 {{:gref lib:trocq.map0}}.
+map->class map1 {{:gref lib:trocq.map1}}.
+map->class map2a {{:gref lib:trocq.map2a}}.
+map->class map2b {{:gref lib:trocq.map2b}}.
+map->class map3 {{:gref lib:trocq.map3}}.
+map->class map4 {{:gref lib:trocq.map4}}.
+
+pred map-class->indc-class o:map-class, o:gref.
+map-class->indc-class map0 {{:gref lib:trocq.indc_map0}}.
+map-class->indc-class map1 {{:gref lib:trocq.indc_map1}}.
+map-class->indc-class map2a {{:gref lib:trocq.indc_map2a}}.
+map-class->indc-class map2b {{:gref lib:trocq.indc_map2b}}.
+map-class->indc-class map3 {{:gref lib:trocq.indc_map3}}.
+map-class->indc-class map4 {{:gref lib:trocq.indc_map4}}.
+
 pred map-class->term i:map-class, o:term.
-map-class->term map0 (pglobal Map0 UI) :-
-  coq.locate "map0" Map0,
-  coq.univ-instance UI [].
-map-class->term map1 (pglobal Map1 UI) :-
-  coq.locate "map1" Map1,
-  coq.univ-instance UI [].
-map-class->term map2a (pglobal Map2a UI) :-
-  coq.locate "map2a" Map2a,
-  coq.univ-instance UI [].
-map-class->term map2b (pglobal Map2b UI) :-
-  coq.locate "map2b" Map2b,
-  coq.univ-instance UI [].
-map-class->term map3 (pglobal Map3 UI) :-
-  coq.locate "map3" Map3,
-  coq.univ-instance UI [].
-map-class->term map4 (pglobal Map4 UI) :-
-  coq.locate "map4" Map4,
-  coq.univ-instance UI [].
+map-class->term Class (pglobal Map UI) :- std.do! [
+  map-class->indc-class Class Map, coq.univ-instance UI [] ].
 
 pred term->map-class i:term, o:map-class.
-term->map-class (pglobal Map0 _)  map0  :- coq.locate "map0"  Map0.
-term->map-class (pglobal Map1 _)  map1  :- coq.locate "map1"  Map1.
-term->map-class (pglobal Map2a _) map2a :- coq.locate "map2a" Map2a.
-term->map-class (pglobal Map2b _) map2b :- coq.locate "map2b" Map2b.
-term->map-class (pglobal Map3 _)  map3  :- coq.locate "map3"  Map3.
-term->map-class (pglobal Map4 _)  map4  :- coq.locate "map4"  Map4.
+term->map-class (pglobal Map _) Class :- map-class->indc-class Class Map.
 
 pred map-class->string i:map-class, o:string.
 map-class->string map0  "0".
@@ -62,10 +73,19 @@ map-class->string map2b "2b".
 map-class->string map3  "3".
 map-class->string map4  "4".
 
+
 pred param-class->string i:param-class, o:string.
 param-class->string (pc M N) S :-
   S is {map-class->string M} ^ {map-class->string N}.
 
+pred param-class->add-suffix i:param-class, i:string, o:string.
+param-class->add-suffix Class P S :- S is P ^ {param-class->string Class}.
+
+pred param-class->add-2-suffix i:string,
+  i:param-class, i:param-class, i:string, o:string.
+param-class->add-2-suffix Sep Class1 Class2 P S :-
+   S is P ^ {param-class->string Class1} ^ Sep ^ {param-class->string Class2}.
+
 % names of the fields contained in a witness of a given level
 pred map-class->fields i:map-class, o:list string.
 map-class->fields map0  [].
diff --git a/theories/Database.v b/theories/Database.v
index 1840c5d..c1ecc92 100644
--- a/theories/Database.v
+++ b/theories/Database.v
@@ -20,11 +20,18 @@ Set Universe Polymorphism.
 Unset Universe Minimization ToSet.
 
 Elpi Db trocq.db lp:{{
+
+  % trocq.db.rel (pc M N) {{ParamMN.Rel}} {{ParamMN.BuildRel}}
+  %   {{ParamMN.R}} {{ParamMN.covariant}} {{ParamMN.contravariant}}
+  pred trocq.db.rel o:param-class, o:gref, o:gref,
+    o:gref, o:gref, o:gref.
+
   pred trocq.db.r o:param-class, o:constant.
   :name "default-r"
   trocq.db.r C R :- var C, !,
     declare_constraint (trocq.db.r C R) [C].
 
+  % subsummed by trocq.db.rel
   pred trocq.db.gref->class o:gref, o:param-class.
 
   pred trocq.db.ptype o:constant.
@@ -66,4 +73,5 @@ Elpi Db trocq.db lp:{{
   :name "default-gref"
   trocq.db.gref _ _ _ _ _ :- do-not-fail, !, false.
   trocq.db.gref GR Out _ _ _ :- coq.error "cannot find" GR "at out class" Out.
+
 }}.
diff --git a/theories/Hierarchy.v b/theories/Hierarchy.v
index efdf1fb..c870d16 100644
--- a/theories/Hierarchy.v
+++ b/theories/Hierarchy.v
@@ -24,6 +24,17 @@ Unset Universe Minimization ToSet.
 
 Set Polymorphic Inductive Cumulativity.
 
+Inductive map_class : Set := map0 | map1 | map2a | map2b | map3 | map4.
+
+Register map0 as trocq.indc_map0.
+Register map1 as trocq.indc_map1.
+Register map2a as trocq.indc_map2a.
+Register map2b as trocq.indc_map2b.
+Register map3 as trocq.indc_map3.
+Register map4 as trocq.indc_map4.
+Register sym_rel as trocq.sym_rel.
+Register paths as trocq.paths.
+
 (*************************)
 (* Parametricity Classes *)
 (*************************)
@@ -71,14 +82,37 @@ Record Has@{i} {A B : Type@{i}} (R : A -> B -> Type@{i}) := BuildHas {
 }.
 End Map4.
 
-(********************)
-(* Record Hierarchy *)
-(********************)
+Register Map0.Has as trocq.map0.
+Register Map1.Has as trocq.map1.
+Register Map2a.Has as trocq.map2a.
+Register Map2b.Has as trocq.map2b.
+Register Map3.Has as trocq.map3.
+Register Map4.Has as trocq.map4.
+Register sym_rel as trocq.sym_rel.
+
+Definition PType@{i} (m n : map_class) (* : Type@{i+1} *) := Type@{i}.
+Definition weaken@{i} (m n m' n' : map_class) {A : Type@{i}} (a : A) : A := a.
+Register PType as trocq.ptype.
+Register weaken as trocq.weaken.
 
 Elpi Command genhierarchy.
 Elpi Accumulate File util.
 Elpi Accumulate Db trocq.db.
 Elpi Accumulate File param_class.
+Elpi Accumulate File util.
+
+Elpi Query lp:{{
+  {{:gref lib:trocq.ptype}} = const PType,
+  coq.elpi.accumulate _ "trocq.db" (clause _ _ (trocq.db.ptype PType)),
+  {{:gref lib:trocq.weaken}} = const Weaken,
+  coq.elpi.accumulate _ "trocq.db" (clause _ _ (trocq.db.weaken Weaken)).
+}}.
+Elpi Typecheck.
+
+(********************)
+(* Record Hierarchy *)
+(********************)
+
 Elpi Accumulate lp:{{
   % generate a module with a record type containing:
   % - a relation R : A -> B -> Type;
@@ -87,56 +121,60 @@ Elpi Accumulate lp:{{
   % (projections are generated so that all fields are accessible from the top record)
   pred generate-module i:param-class, i:univ, i:univ.variable.
   generate-module (pc M N as Class) U L :-
-    map-class->string M MStr,
-    map-class->string N NStr,
     % open module
-    coq.env.begin-module {calc ("Param" ^ MStr ^ NStr)} none,
+    coq.env.begin-module {param-class->add-suffix Class "Param"} none,
     % generate record
     coq.univ-instance UI [L],
-    coq.locate {calc ("Map" ^ MStr ^ ".Has")} CovariantSubRecord,
-    coq.locate {calc ("Map" ^ NStr ^ ".Has")} ContravariantSubRecord,
-    coq.locate "sym_rel" SymRel,
+    map->class M CovariantSubRecord,
+    map->class N ContravariantSubRecord,
+    SymRel = {sym-rel},
+    TypeU = sort (typ U),
     RelDecl =
-      parameter "A" _ (sort (typ U)) (a\
-        parameter "B" _ (sort (typ U)) (b\
+      parameter "A" _ TypeU (a\
+        parameter "B" _ TypeU (b\
           record "Rel" (sort (typ {coq.univ.super U})) "BuildRel" (
-            field [] "R" {{ lp:a -> lp:b -> lp:{{ sort (typ U) }} }} (r\
-            field [] "covariant" (app [pglobal CovariantSubRecord UI, a, b, r]) (_\
+            field [] "R" {{ lp:a -> lp:b -> lp:{{ sort (typ U) }} }} r\
+            field [] "covariant" (app [pglobal CovariantSubRecord UI, a, b, r]) _\
             field [] "contravariant"
               (app [pglobal ContravariantSubRecord UI, b, a, app [pglobal SymRel UI, a, b, r]]) (_\
-          end-record)))))),
-    @primitive! => @udecl! [L] ff [] ff => coq.env.add-indt RelDecl TrocqInd,
-    coq.locate "Rel" Rel,
-    coq.locate "R" R,
+          end-record)))),
+    @primitive! => @udecl! [L] ff [] ff => coq.env.add-indt RelDecl TrocqInd,coq.env.indt TrocqInd _ _ _ _ [TrocqBuild] _,
+    Rel = indt TrocqInd,
+    coq.env.projections TrocqInd
+      [some CR, some CovariantProj, some ContravariantProj],
     % add R to database for later use
     R = const CR,
     coq.elpi.accumulate _ "trocq.db"
       (clause _ (after "default-r") (trocq.db.r Class CR)),
     coq.elpi.accumulate execution-site "trocq.db"
       (clause _ _ (trocq.db.gref->class (indt TrocqInd) Class)),
+    coq.elpi.accumulate execution-site "trocq.db"
+      (clause _ _ (trocq.db.rel Class (indt TrocqInd) (indc TrocqBuild)
+        (const CR) (const CovariantProj) (const ContravariantProj))),
     % generate projections on the covariant subrecord
     map-class->fields M MFields,
-    coq.locate "covariant" Covariant,
-    std.forall MFields (field\ sigma FieldName Field Decl\
-      FieldName is "Map" ^ MStr ^ "." ^ field,
-      coq.locate FieldName Field,
+    CovariantSubRecord = indt CovariantSubRecordIndt,
+    coq.env.projections CovariantSubRecordIndt MSomeProjs,
+    Covariant = const CovariantProj,
+    std.forall2 MFields MSomeProjs (field-name\ some-pr\ sigma Decl Pr\
+      some-pr = some Pr,
       Decl =
         (fun `A` (sort (typ U)) a\ fun `B` (sort (typ U)) b\ fun `P` (app [pglobal Rel UI, a, b]) p\
-          app [pglobal Field UI, a, b,
+          app [pglobal (const Pr) UI, a, b,
             app [pglobal R UI, a, b, p], app [pglobal Covariant UI, a, b, p]]),
-      @udecl! [L] ff [] ff => coq.env.add-const field Decl _ @transparent! _
+      @udecl! [L] ff [] ff => coq.env.add-const field-name Decl _ @transparent! _
     ),
     % generate projections on the contravariant subrecord
-    map-class->fields N NFields,
     map-class->cofields N NCoFields,
-    coq.locate "contravariant" Contravariant,
-    std.forall2 NFields NCoFields (field\ field-name\ sigma FieldName Field Decl\
-      FieldName is "Map" ^ NStr ^ "." ^ field,
-      coq.locate FieldName Field,
+    Contravariant = const ContravariantProj,
+    ContravariantSubRecord = indt ContravariantSubRecordIndt,
+    coq.env.projections ContravariantSubRecordIndt NSomeProjs,
+    std.forall2 NCoFields NSomeProjs (field-name\ some-pr\ sigma Decl Pr\
+      some-pr = some Pr,
       Decl =
         (fun `A` (sort (typ U)) a\ fun `B` (sort (typ U)) b\
           fun `P` (app [pglobal Rel UI, a, b]) p\
-            app [pglobal Field UI, b, a,
+            app [pglobal (const Pr) UI, b, a,
               app [pglobal SymRel UI, a, b, app [pglobal R UI, a, b, p]],
               app [pglobal Contravariant UI, a, b, p]]),
       @udecl! [L] ff [] ff => coq.env.add-const field-name Decl _ @transparent! _
@@ -150,27 +188,27 @@ Elpi Typecheck.
 (* Record Weakening *)
 (********************)
 
-Definition forgetMap43@{i}
+Coercion forgetMap43@{i}
   {A B : Type@{i}} {R : A -> B -> Type@{i}} (m : Map4.Has@{i} R) : Map3.Has@{i} R :=
     @Map3.BuildHas A B R (@Map4.map A B R m) (@Map4.map_in_R A B R m) (@Map4.R_in_map A B R m).
 
-Definition forgetMap32a@{i}
+Coercion forgetMap32a@{i}
   {A B : Type@{i}} {R : A -> B -> Type@{i}} (m : Map3.Has@{i} R) : Map2a.Has@{i} R :=
     @Map2a.BuildHas A B R (@Map3.map A B R m) (@Map3.map_in_R A B R m).
 
-Definition forgetMap32b@{i}
+Coercion forgetMap32b@{i}
   {A B : Type@{i}} {R : A -> B -> Type@{i}} (m : Map3.Has@{i} R) : Map2b.Has@{i} R :=
     @Map2b.BuildHas A B R (@Map3.map A B R m) (@Map3.R_in_map A B R m).
 
-Definition forgetMap2a1@{i}
+Coercion forgetMap2a1@{i}
   {A B : Type@{i}} {R : A -> B -> Type@{i}} (m : Map2a.Has@{i} R) : Map1.Has@{i} R :=
     @Map1.BuildHas A B R (@Map2a.map A B R m).
 
-Definition forgetMap2b1@{i}
+Coercion forgetMap2b1@{i}
   {A B : Type@{i}} {R : A -> B -> Type@{i}} (m : Map2b.Has@{i} R) : Map1.Has@{i} R :=
     @Map1.BuildHas A B R (@Map2b.map A B R m).
 
-Definition forgetMap10@{i}
+Coercion forgetMap10@{i}
   {A B : Type@{i}} {R : A -> B -> Type@{i}} (m : Map1.Has@{i} R) : Map0.Has@{i} R :=
     @Map0.BuildHas A B R.
 
@@ -178,25 +216,18 @@ Elpi Accumulate lp:{{
   % generate 2 functions of weakening per possible weakening:
   % one on the left and one on the right, if possible
   pred generate-forget i:param-class, i:univ, i:univ.variable.
-  generate-forget (pc M N) U L :-
+  generate-forget (pc M N as Class) U L :-
     coq.univ-instance UI [L],
-    map-class->string M MStr,
-    map-class->string N NStr,
-    ModuleNameMN is "Param" ^ MStr ^ NStr,
-    coq.locate {calc (ModuleNameMN ^ ".Rel")} RelMN,
-    coq.locate {calc (ModuleNameMN ^ ".R")} RMN,
-    coq.locate {calc (ModuleNameMN ^ ".covariant")} CovariantMN,
-    coq.locate {calc (ModuleNameMN ^ ".contravariant")} ContravariantMN,
+    map->class M MGR,
+    map->class N NGR,
+    trocq.db.rel Class RelMN _ RMN CovariantMN ContravariantMN,
     % covariant weakening
     std.forall {map-class.weakenings-from M} (m1\
-      sigma M1Str ModuleNameM1N BuildRelName BuildRelM1N ForgetMapName
-            ForgetMapM Decl ForgetName Forget RelName RelM1N\ std.do! [
-        map-class->string m1 M1Str,
-        ModuleNameM1N is "Param" ^ M1Str ^ NStr,
-        BuildRelName is ModuleNameM1N ^ ".BuildRel",
-        coq.locate BuildRelName BuildRelM1N,
-        ForgetMapName is "forgetMap" ^ MStr ^ M1Str,
-        coq.locate ForgetMapName ForgetMapM,
+      sigma BuildRelM1N ForgetMapM Decl ForgetName ForgetCst M1GR RelM1N\
+      std.do! [
+        map->class m1 M1GR,
+        trocq.db.rel (pc m1 N) RelM1N BuildRelM1N _ _ _,
+        coq.coercion.db-for (grefclass MGR) (grefclass M1GR) [pr ForgetMapM _],
         Decl =
           (fun `A` (sort (typ U)) a\ fun `B` (sort (typ U)) b\
             fun `P` (app [pglobal RelMN UI, a, b]) p\
@@ -204,25 +235,20 @@ Elpi Accumulate lp:{{
                 app [pglobal ForgetMapM UI, a, b, app [pglobal RMN UI, a, b, p],
                   app [pglobal CovariantMN UI, a, b, p]],
                 app [pglobal ContravariantMN UI, a, b, p]]),
-        ForgetName is "forget_" ^ MStr ^ NStr ^ "_" ^ M1Str ^ NStr,
+        param-class->add-2-suffix "_" Class (pc m1 N) "forget_" ForgetName,
         @udecl! [L] ff [] ff =>
-          coq.env.add-const ForgetName Decl _ @transparent! _,
-        coq.locate ForgetName Forget,
-        RelName is ModuleNameM1N ^ ".Rel",
-        coq.locate RelName RelM1N,
-        @global! => coq.coercion.declare (coercion Forget 2 RelMN (grefclass RelM1N))
+          coq.env.add-const ForgetName Decl _ @transparent! ForgetCst,
+        @global! => coq.coercion.declare
+          (coercion (const ForgetCst) 2 RelMN (grefclass RelM1N))
     ]),
     % contravariant weakening
-    coq.locate "sym_rel" SymRel,
+    SymRel = {sym-rel},
     std.forall {map-class.weakenings-from N} (n1\
-      sigma N1Str ModuleNameMN1 BuildRelName BuildRelMN1 ForgetMapName
-            ForgetMapN Decl ForgetName Forget RelName RelMN1\ std.do! [
-        map-class->string n1 N1Str,
-        ModuleNameMN1 is "Param" ^ MStr ^ N1Str,
-        BuildRelName is ModuleNameMN1 ^ ".BuildRel",
-        coq.locate BuildRelName BuildRelMN1,
-        ForgetMapName is "forgetMap" ^ NStr ^ N1Str,
-        coq.locate ForgetMapName ForgetMapN,
+      sigma BuildRelMN1 ForgetMapN Decl ForgetName ForgetCst N1GR RelMN1\
+      std.do! [
+        map->class n1 N1GR,
+        trocq.db.rel (pc M n1) RelMN1 BuildRelMN1 _ _ _,
+        coq.coercion.db-for (grefclass NGR) (grefclass N1GR) [pr ForgetMapN _],
         Decl =
           (fun `A` (sort (typ U)) a\ fun `B` (sort (typ U)) b\
             fun `P` (app [pglobal RelMN UI, a, b]) p\
@@ -231,13 +257,11 @@ Elpi Accumulate lp:{{
                 app [pglobal ForgetMapN UI, b, a,
                   app [pglobal SymRel UI, a, b, app [pglobal RMN UI, a, b, p]],
                   app [pglobal ContravariantMN UI, a, b, p]]]),
-        ForgetName is "forget_" ^ MStr ^ NStr ^ "_" ^ MStr ^ N1Str,
+        param-class->add-2-suffix "_" Class (pc M n1) "forget_" ForgetName,
         @udecl! [L] ff [] ff =>
-          coq.env.add-const ForgetName Decl _ @transparent! _,
-        coq.locate ForgetName Forget,
-        RelName is ModuleNameMN1 ^ ".Rel",
-        coq.locate RelName RelMN1,
-        @global! => coq.coercion.declare (coercion Forget 2 RelMN (grefclass RelMN1))
+          coq.env.add-const ForgetName Decl _ @transparent! ForgetCst,
+        @global! => coq.coercion.declare
+          (coercion (const ForgetCst) 2 RelMN (grefclass RelMN1))
     ]).
 }}.
 Elpi Typecheck.
@@ -246,15 +270,24 @@ Elpi Typecheck.
 Elpi Query lp:{{
   coq.univ.new U,
   coq.univ.variable U L,
-  Classes = [map0, map1, map2a, map2b, map3, map4],
+  map-classes all Classes,
   std.forall Classes (m\
     std.forall Classes (n\
-      generate-module (pc m n) U L,
-      generate-forget (pc m n) U L
+      generate-module (pc m n) U L
     )
   ).
 }}.
 
+Elpi Query lp:{{
+  coq.univ.new U,
+  coq.univ.variable U L,
+  map-classes all Classes,
+  std.forall Classes (m\
+    std.forall Classes (n\
+      generate-forget (pc m n) U L
+    )
+  ).
+}}.
 (* Set Printing Universes. Print Module Param2a3. *)
 (* Set Printing Universes. Print forget_42b_41. *)
 (* Check forall (p : Param44.Rel nat nat), @paths (Param12a.Rel nat nat) p p. *)
@@ -578,14 +611,15 @@ Defined.
 
 (* generate id_ParamMN : forall A, ParamMN.Rel A A for all M N *)
 
+
 Elpi Accumulate lp:{{
   pred generate-id-param i:param-class, i:univ, i:univ.variable.
-  generate-id-param (pc M N) U L :-
+  generate-id-param (pc M N as Class) U L :-
     map-class->string M MStr,
     map-class->string N NStr,
     coq.univ-instance UI [L],
-    coq.locate {calc ("Param" ^ MStr ^ NStr ^ ".BuildRel")} BuildRel,
-    coq.locate "paths" Paths,
+    trocq.db.rel Class _ BuildRel _ _ _,
+    Paths = {paths},
     coq.locate {calc ("id_Map" ^ MStr)} IdMap,
     coq.locate {calc ("id_Map" ^ NStr ^ "_sym")} IdMapSym,
     Decl =
@@ -601,7 +635,7 @@ Elpi Typecheck.
 Elpi Query lp:{{
   coq.univ.new U,
   coq.univ.variable U L,
-  Classes = [map0, map1, map2a, map2b, map3, map4],
+  map-classes all Classes,
   std.forall Classes (m\
     std.forall Classes (n\
       generate-id-param (pc m n) U L
@@ -616,17 +650,13 @@ Elpi Query lp:{{
 
 Elpi Accumulate lp:{{
   pred generate-param-sym i:param-class, i:univ, i:univ.variable.
-  generate-param-sym (pc M N) U L :-
+  generate-param-sym (pc M N as Class) U L :-
     map-class->string M MStr,
     map-class->string N NStr,
     coq.univ-instance UI [L],
-    coq.locate {calc ("Param" ^ MStr ^ NStr ^ ".Rel")} RelMN,
-    coq.locate {calc ("Param" ^ NStr ^ MStr ^ ".BuildRel")} BuildRelNM,
-    coq.locate "sym_rel" SymRel,
-    coq.locate {calc ("Param" ^ MStr ^ NStr ^ ".R")} RMN,
-    coq.locate {calc ("Param" ^ MStr ^ NStr ^ ".covariant")} CovariantMN,
-    coq.locate
-      {calc ("Param" ^ MStr ^ NStr ^ ".contravariant")} ContravariantMN,
+    trocq.db.rel Class RelMN _ RMN CovariantMN ContravariantMN,
+    trocq.db.rel (pc N M) _ BuildRelNM _ _ _,
+    SymRel = {sym-rel},
     Decl =
       (fun `A` (sort (typ U)) a\ fun `B` (sort (typ U)) b\
         fun `P` (app [pglobal RelMN UI, a, b]) p\
@@ -643,7 +673,7 @@ Elpi Typecheck.
 Elpi Query lp:{{
   coq.univ.new U,
   coq.univ.variable U L,
-  Classes = [map0, map1, map2a, map2b, map3, map4],
+  map-classes all Classes,
   std.forall Classes (m\
     std.forall Classes (n\
       generate-param-sym (pc m n) U L
diff --git a/theories/Param.v b/theories/Param.v
index 8a4ca07..5708596 100644
--- a/theories/Param.v
+++ b/theories/Param.v
@@ -29,8 +29,6 @@ From Trocq.Elpi.constraints Extra Dependency "constraints.elpi" as constraints.
 Set Universe Polymorphism.
 Unset Universe Minimization ToSet.
 
-Inductive map_class : Set := map0 | map1 | map2a | map2b | map3 | map4.
-
 (* PType and weaken *)
 
 Elpi Command genpparam.
@@ -38,15 +36,6 @@ Elpi Accumulate File util.
 Elpi Accumulate Db trocq.db.
 Elpi Accumulate File param_class.
 
-Definition PType@{i} (m n : map_class) (* : Type@{i+1} *) := Type@{i}.
-Definition weaken@{i} (m n m' n' : map_class) {A : Type@{i}} (a : A) : A := a.
-
-Elpi Query lp:{{
-  coq.locate "PType" (const PType),
-  coq.elpi.accumulate _ "trocq.db" (clause _ _ (trocq.db.ptype PType)),
-  coq.locate "weaken" (const Weaken),
-  coq.elpi.accumulate _ "trocq.db" (clause _ _ (trocq.db.weaken Weaken)).
-}}.
 
 (* generate
   PParamMN_Type P Q := ParamMN_TypePQ for all M N under 2b
@@ -67,7 +56,7 @@ Elpi Accumulate lp:{{
   pred generate-match2
     i:term, i:univ-instance, i:param-class, i:term, i:map-class, o:term.
   generate-match2 RetType UI2 Class QVar P Match :-
-    std.map [map0, map1, map2a, map2b, map3, map4]
+    map-classes all Classes, std.map Classes
       (q\ b\ generate-branch UI2 Class (pc P q) b) Branches,
     coq.locate "map_class" MapClass,
     coq.univ-instance UI0 [],
@@ -76,7 +65,7 @@ Elpi Accumulate lp:{{
   pred generate-match1
     i:term, i:univ-instance, i:param-class, i:term, i:term, o:term.
   generate-match1 RetType UI2 Class PVar QVar Match :-
-    std.map [map0, map1, map2a, map2b, map3, map4]
+    map-classes all Classes, std.map Classes
       (p\ b\ generate-match2 RetType UI2 Class QVar p b) Branches,
     coq.locate "map_class" MapClass,
     coq.univ-instance UI0 [],
@@ -118,9 +107,9 @@ Elpi Query lp:{{
   coq.univ.variable U L,
   coq.univ.super U U1,
   coq.univ.variable U1 L1,
-  Classes1 = [map0, map1, map2a],
-  Classes2 = [map2b, map3, map4],
-  Classes = [map0, map1, map2a, map2b, map3, map4],
+  map-classes low Classes1,
+  map-classes high Classes2,
+  map-classes all Classes,
   % first the ones where the arguments matter
   std.forall Classes1 (m\
     std.forall Classes1 (n\
diff --git a/theories/Param_Type.v b/theories/Param_Type.v
index fbec6c4..25cfdca 100644
--- a/theories/Param_Type.v
+++ b/theories/Param_Type.v
@@ -91,8 +91,9 @@ Elpi Query lp:{{
   coq.univ.super U U1,
   % cannot have only one binder in the declaration because this line creates a fresh level:
   coq.univ.variable U1 L1,
-  Classes = [map0, map1, map2a, map2b, map3, map4],
-  std.forall [map0, map1, map2a] (m\
+  map-classes all Classes,
+  map-classes low LowClasses,
+  std.forall LowClasses (m\
     std.forall Classes (n\
       std.forall Classes (p\
         generate-map-type m (pc n p) U L L1
@@ -232,9 +233,9 @@ Elpi Query lp:{{
   coq.univ.super U U1,
   % cannot have only one binder in the declaration because this line creates a fresh level:
   coq.univ.variable U1 L1,
-  AllClasses = [map0, map1, map2a, map2b, map3, map4],
-  Classes__ = [map0, map1, map2a],
-  Classes44 = [map2b, map3, map4],
+  map-classes all AllClasses,
+  map-classes low Classes__,
+  map-classes high Classes44,
   std.forall Classes__ (m\
     std.forall Classes__ (n\
       std.forall AllClasses (p\
diff --git a/theories/Param_arrow.v b/theories/Param_arrow.v
index d5bb3b9..197cbdd 100644
--- a/theories/Param_arrow.v
+++ b/theories/Param_arrow.v
@@ -265,7 +265,7 @@ Elpi Query lp:{{
   coq.univ.max Ui Uj Uk,
   % cannot have only 2 binders in the declaration because this line creates a fresh level:
   coq.univ.variable Uk Lk,
-  Classes = [map0, map1, map2a, map2b, map3, map4],
+  map-classes all Classes,
   std.forall Classes (m\
     std.forall Classes (n\
       generate-param-arrow (pc m n) Ui Uj Li Lj Lk
diff --git a/theories/Param_forall.v b/theories/Param_forall.v
index 1178286..4765cfb 100644
--- a/theories/Param_forall.v
+++ b/theories/Param_forall.v
@@ -326,7 +326,7 @@ Elpi Query lp:{{
   coq.univ.max Ui Uj Uk,
   % cannot have only 2 binders in the declaration because this line creates a fresh level:
   coq.univ.variable Uk Lk,
-  Classes = [map0, map1, map2a, map2b, map3, map4],
+  map-classes all Classes,
   std.forall Classes (m\
     std.forall Classes (n\
       generate-param-forall (pc m n) Ui Uj Li Lj Lk