diff --git a/.nix/config.nix b/.nix/config.nix
new file mode 100644
index 0000000..b664596
--- /dev/null
+++ b/.nix/config.nix
@@ -0,0 +1,102 @@
+{
+  ## DO NOT CHANGE THIS
+  format = "1.0.0";
+  ## unless you made an automated or manual update
+  ## to another supported format.
+
+  ## The attribute to build from the local sources,
+  ## either using nixpkgs data or the overlays located in `.nix/coq-overlays`
+  ## Will determine the default main-job of the bundles defined below
+  attribute = "trocq";
+
+  ## If you want to select a different attribute (to build from the local sources as well)
+  ## when calling `nix-shell` and `nix-build` without the `--argstr job` argument
+  # shell-attribute = "{{nix_name}}";
+
+  ## Maybe the shortname of the library is different from
+  ## the name of the nixpkgs attribute, if so, set it here:
+  # pname = "{{shortname}}";
+
+  ## Lists the dependencies, phrased in terms of nix attributes.
+  ## No need to list Coq, it is already included.
+  ## These dependencies will systematically be added to the currently
+  ## known dependencies, if any more than Coq.
+  ## /!\ Remove this field as soon as the package is available on nixpkgs.
+  ## /!\ Manual overlays in `.nix/coq-overlays` should be preferred then.
+  # buildInputs = [ ];
+
+  ## Indicate the relative location of your _CoqProject
+  ## If not specified, it defaults to "_CoqProject"
+  # coqproject = "_CoqProject";
+
+  ## select an entry to build in the following `bundles` set
+  ## defaults to "default"
+  default-bundle = "default";
+
+  ## write one `bundles.name` attribute set per
+  ## alternative configuration
+  ## When generating GitHub Action CI, one workflow file
+  ## will be created per bundle
+  bundles.default = {
+
+    ## You can override Coq and other Coq coqPackages
+    ## through the following attribute
+    coqPackages.coq.override.version = "8.17";
+    coqPackages.coq-elpi.override.version = "ecranceMERCE:strat";
+
+    ## In some cases, light overrides are not available/enough
+    ## in which case you can use either
+    # coqPackages.<coq-pkg>.overrideAttrs = o: <overrides>;
+    ## or a "long" overlay to put in `.nix/coq-overlays
+    ## you may use `nix-shell --run fetchOverlay <coq-pkg>`
+    ## to automatically retrieve the one from nixpkgs
+    ## if it exists and is correctly named/located
+
+    ## You can override Coq and other coqPackages
+    ## through the following attribute
+    ## If <ocaml-pkg> does not support light overrides,
+    ## you may use `overrideAttrs` or long overlays
+    ## located in `.nix/ocaml-overlays`
+    ## (there is no automation for this one)
+    #  ocamlPackages.<ocaml-pkg>.override.version = "x.xx";
+
+    ## You can also override packages from the nixpkgs toplevel
+    # <nix-pkg>.override.overrideAttrs = o: <overrides>;
+    ## Or put an overlay in `.nix/overlays`
+
+    ## you may mark a package as a main CI job (one to take deps and
+    ## rev deps from) as follows
+    # coqPackages.<main-pkg>.main-job = true;
+    ## by default the current package and its shell attributes are main jobs
+
+    ## you may mark a package as a CI job as follows
+    #  coqPackages.<another-pkg>.job = "test";
+    ## It can then built through
+    ## nix-build --argstr bundle "default" --arg job "test";
+    ## in the absence of such a directive, the job "another-pkg" will
+    ## is still available, but will be automatically included in the CI
+    ## via the command genNixActions only if it is a dependency or a
+    ## reverse dependency of a job flagged as "main-job" (see above).
+
+  };
+
+  ## Cachix caches to use in CI
+  ## Below we list some standard ones
+  cachix.coq = {};
+  cachix.math-comp = {};
+  cachix.coq-community = {};
+  
+  ## If you have write access to one of these caches you can
+  ## provide the auth token or signing key through a secret
+  ## variable on GitHub. Then, you should give the variable
+  ## name here. For instance, coq-community projects can use
+  ## the following line instead of the one above:
+  # cachix.coq-community.authToken = "CACHIX_AUTH_TOKEN";
+  
+  ## Or if you have a signing key for a given Cachix cache:
+  # cachix.my-cache.signingKey = "CACHIX_SIGNING_KEY"
+  
+  ## Note that here, CACHIX_AUTH_TOKEN and CACHIX_SIGNING_KEY
+  ## are the names of secret variables. They are set in
+  ## GitHub's web interface.
+}
diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix
new file mode 100644
index 0000000..60b452b
--- /dev/null
+++ b/.nix/coq-nix-toolbox.nix
@@ -0,0 +1 @@
+"f72eef6033e0abc9fa06f94fe718d8aa9c0d031a"
diff --git a/.nix/coq-overlays/HoTT/default.nix b/.nix/coq-overlays/HoTT/default.nix
new file mode 100644
index 0000000..997fecb
--- /dev/null
+++ b/.nix/coq-overlays/HoTT/default.nix
@@ -0,0 +1,46 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+
+mkCoqDerivation {
+  pname = "HoTT";
+  repo = "Coq-HoTT";
+  owner = "HoTT";
+  inherit version;
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
+    { case = range "8.14" "8.17"; out = coq.coq-version; }
+  ] null;
+  releaseRev = v: "V${v}";
+  release."8.14".sha256 = "sha256-7kXk2pmYsTNodHA+Qts3BoMsewvzmCbYvxw9Sgwyvq0=";
+  release."8.15".sha256 = "sha256-JfeiRZVnrjn3SQ87y6dj9DWNwCzrkK3HBogeZARUn9g=";
+  release."8.16".sha256 = "sha256-xcEbz4ZQ+U7mb0SEJopaczfoRc2GSgF2BGzUSWI0/HY=";
+  release."8.17".sha256 = "sha256-GjTUpzL9UzJm4C2ilCaYEufLG3hcj7rJPc5Op+OMal8=";
+
+  # versions of HoTT for Coq 8.17 and onwards will use dune
+  # opam-name = if lib.versions.isLe "8.17" coq.coq-version then "coq-hott" else null;
+  opam-name = "coq-hott";
+  useDune = lib.versions.isGe "8.17" coq.coq-version;
+  
+  patchPhase = ''
+    patchShebangs etc
+  '';
+
+  meta = {
+    homepage = "https://homotopytypetheory.org/";
+    description = "The Homotopy Type Theory library";
+    longDescription = ''
+      Homotopy Type Theory is an interpretation of Martin-Löf’s intensional
+      type theory into abstract homotopy theory. Propositional equality is
+      interpreted as homotopy and type isomorphism as homotopy equivalence.
+      Logical constructions in type theory then correspond to
+      homotopy-invariant constructions on spaces, while theorems and even
+      proofs in the logical system inherit a homotopical meaning. As the
+      natural logic of homotopy, type theory is also related to higher
+      category theory as it is used e.g. in the notion of a higher topos.
+
+      The HoTT library is a development of homotopy-theoretic ideas in the Coq
+      proof assistant. It draws many ideas from Vladimir Voevodsky's
+      Foundations library (which has since been incorporated into the Unimath
+      library) and also cross-pollinates with the HoTT-Agda library.
+    '';
+    maintainers = with lib.maintainers; [ alizter siddharthist ];
+  };
+}
diff --git a/.nix/coq-overlays/coq-elpi/default.nix b/.nix/coq-overlays/coq-elpi/default.nix
new file mode 100644
index 0000000..2d4691b
--- /dev/null
+++ b/.nix/coq-overlays/coq-elpi/default.nix
@@ -0,0 +1,64 @@
+{ lib, mkCoqDerivation, which, coq, version ? null }:
+
+with builtins; with lib; let
+  elpi = coq.ocamlPackages.elpi.override (lib.switch coq.coq-version [
+    { case = "8.11"; out = { version = "1.11.4"; };}
+    { case = "8.12"; out = { version = "1.12.0"; };}
+    { case = "8.13"; out = { version = "1.13.7"; };}
+    { case = "8.14"; out = { version = "1.13.7"; };}
+    { case = "8.15"; out = { version = "1.15.0"; };}
+    { case = "8.16"; out = { version = "1.16.5"; };}
+  ] {} );
+in mkCoqDerivation {
+  pname = "elpi";
+  repo  = "coq-elpi";
+  owner = "LPCIC";
+  inherit version;
+  defaultVersion = lib.switch coq.coq-version [
+    { case = "8.16"; out = "1.15.1"; }
+    { case = "8.15"; out = "1.14.0"; }
+    { case = "8.14"; out = "1.11.2"; }
+    { case = "8.13"; out = "1.11.1"; }
+    { case = "8.12"; out = "1.8.3_8.12"; }
+    { case = "8.11"; out = "1.6.3_8.11"; }
+  ] null;
+  release."1.15.1".sha256     = "sha256-NT2RlcIsFB9AvBhMxil4ZZIgx+KusMqDflj2HgQxsZg=";
+  release."1.14.0".sha256     = "sha256:1v2p5dlpviwzky2i14cj7gcgf8cr0j54bdm9fl5iz1ckx60j6nvp";
+  release."1.13.0".sha256     = "1j7s7dlnjbw222gnbrsjgmjck1yrx7h6hwm8zikcyxi0zys17w7n";
+  release."1.12.1".sha256     = "sha256-4mO6/co7NcIQSGIQJyoO8lNWXr6dqz+bIYPO/G0cPkY=";
+  release."1.11.2".sha256     = "0qk5cfh15y2zrja7267629dybd3irvxk1raz7z8qfir25a81ckd4";
+  release."1.11.1".sha256     = "10j076vc2hdcbm15m6s7b6xdzibgfcbzlkgjnlkr2vv9k13qf8kc";
+  release."1.10.1".sha256     = "1zsyx26dvj7pznfd2msl2w7zbw51q1nsdw0bdvdha6dga7ijf7xk";
+  release."1.9.7".sha256      = "0rvn12h9dpk9s4pxy32p8j0a1h7ib7kg98iv1cbrdg25y5vs85n1";
+  release."1.9.5".sha256      = "0gjdwmb6bvb5gh0a6ra48bz5fb3pr5kpxijb7a8mfydvar5i9qr6";
+  release."1.9.4".sha256      = "0nii7238mya74f9g6147qmpg6gv6ic9b54x5v85nb6q60d9jh0jq";
+  release."1.9.3".sha256      = "198irm800fx3n8n56vx1c6f626cizp1d7jfkrc6ba4iqhb62ma0z";
+  release."1.9.2".sha256      = "1rr2fr8vjkc0is7vh1461aidz2iwkigdkp6bqss4hhv0c3ijnn07";
+  release."1.8.3_8.12".sha256  = "15z2l4zy0qpw0ws7bvsmpmyv543aqghrfnl48nlwzn9q0v89p557";
+  release."1.8.3_8.12".version = "1.8.3";
+  release."1.8.2_8.12".sha256  = "1n6jwcdazvjgj8vsv2r9zgwpw5yqr5a1ndc2pwhmhqfl04b5dk4y";
+  release."1.8.2_8.12".version = "1.8.2";
+  release."1.8.1".sha256      = "1fbbdccdmr8g4wwpihzp4r2xacynjznf817lhijw6kqfav75zd0r";
+  release."1.8.0".sha256      = "13ywjg94zkbki22hx7s4gfm9rr87r4ghsgan23xyl3l9z8q0idd1";
+  release."1.7.0".sha256      = "1ws5cqr0xawv69prgygbl3q6dgglbaw0vc397h9flh90kxaqgyh8";
+  release."1.6.3_8.11".sha256 = "1j340cr2bv95clzzkkfmsjkklham1mj84cmiyprzwv20q89zr1hp";
+  release."1.6.3_8.11".version = "1.6.3";
+  release."1.6.2_8.11".sha256 = "06xrx0ljilwp63ik2sxxr7h617dgbch042xfcnfpy5x96br147rn";
+  release."1.6.2_8.11".version = "1.6.2";
+  release."1.6.1_8.11".sha256 = "0yyyh35i1nb3pg4hw7cak15kj4y6y9l84nwar9k1ifdsagh5zq53";
+  release."1.6.1_8.11".version = "1.6.1";
+  release."1.6.0_8.11".sha256 = "0ahxjnzmd7kl3gl38kyjqzkfgllncr2ybnw8bvgrc6iddgga7bpq";
+  release."1.6.0_8.11".version = "1.6.0";
+  release."1.6.0".sha256      = "0kf99i43mlf750fr7fric764mm495a53mg5kahnbp6zcjcxxrm0b";
+  releaseRev = v: "v${v}";
+
+  mlPlugin = true;
+  propagatedBuildInputs = [ elpi ];
+  buildPhase = "make build";
+
+  meta = {
+    description = "Coq plugin embedding ELPI.";
+    maintainers = [ maintainers.cohencyril ];
+    license = licenses.lgpl21Plus;
+  };
+}
diff --git a/.nix/coq-overlays/trocq/default.nix b/.nix/coq-overlays/trocq/default.nix
new file mode 100644
index 0000000..bba64ff
--- /dev/null
+++ b/.nix/coq-overlays/trocq/default.nix
@@ -0,0 +1,60 @@
+## File initially generated by createOverlay
+## and then supposedly modified manually.
+## Some hints for manual modifications are in the file,
+## but the full doc is on nixos / nix packages website:
+## https://nixos.org/manual/nixpkgs/stable/#sec-language-coq
+
+{ lib, mkCoqDerivation, which, coq, HoTT, coq-elpi
+  ## declare extra dependencies here, to be used in propagateBuildInputs e.g.
+  # , mathcomp, coq-elpi
+  , version ? null }:
+
+with lib; mkCoqDerivation {
+  pname = "trocq";
+  ## you can configure the domain, owner and repository, the default are:
+  # repo = "coq_modular_param";
+  # owner = "coq-community";
+  # domain = "github.com";
+
+  inherit version;
+## The `defaultVersion` attribute is important for nixpkgs but can be kept unchanged
+## for local usage since it will be ignored locally if
+## - this derivation corresponds to the main attribute,
+## - or its version is overridden (by a branch, PR, url or path) in `.nix/config.nix`.
+  defaultVersion = with versions; switch coq.coq-version [
+    ## Example of possible dependencies
+    # { case = range "8.13" "8.14"; out = "1.2.0"; }
+    ## other predicates are `isLe v`, `isLt v`, `isGe v`, `isGt v`, `isEq v` etc
+  ] null;
+
+  ## Declare existing releases
+  ## leave sha256 empty at first and then copy paste
+  ## the resulting sha given by the error message
+  # release."1.1.1".sha256 = "";
+  ## if the tag is not exactly the version number you can amend like this
+  # release."1.1.1".rev = "v1.1.1";
+  ## if a consistent scheme gives the tag from the release number, you can do like this:
+  # releaseRev = v: "v${v}";
+
+  ## Add dependencies in here. In particular you can add
+  ## - arbitrary nix packages (you need to require them at the beginning of the file)
+  ## - Coq packages (require them at the beginning of the file)
+  ## - OCaml packages (use `coq.ocamlPackages.xxx`, no need to require them at the beginning of the file)
+  propagatedBuildInputs = [ HoTT coq-elpi ]; ## e.g. `= [ mathcomp coq-elpi ]`
+
+  ## Does the package contain OCaml code?
+  mlPlugin = true;
+
+  ## Give some meta data
+  ## This is needed for submitting the package to nixpkgs but not required for local use.
+  meta = {
+    ## Describe your package in one sentence
+    # description = "";
+    ## Kindly ask one of these people if they want to be an official maintainer.
+    ## (You might also consider adding yourself to the list of maintainers)
+    # maintainers = with maintainers; [ cohencyril siraben vbgl Zimmi48 ];
+    ## Pick a license from
+    ## https://github.com/NixOS/nixpkgs/blob/master/lib/licenses.nix
+    # license = licenses.mit;
+  };
+}
diff --git a/_CoqProject b/_CoqProject
index 4925924..9bbdf79 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -12,7 +12,11 @@ theories/Param_arrow.v
 theories/Database.v
 theories/Param.v
 theories/Trocq.v
+theories/Vernac.v
 theories/Param_paths.v
+theories/Param_sigma.v
+theories/Param_prod.v
+theories/Param_option.v
 
 examples/Example.v
 examples/int_to_Zp.v
diff --git a/default.nix b/default.nix
new file mode 100644
index 0000000..1a24d7a
--- /dev/null
+++ b/default.nix
@@ -0,0 +1,12 @@
+{ config ? {}, withEmacs ? false, print-env ? false, do-nothing ? false,
+  update-nixpkgs ? false, ci-matrix ? false,
+  override ? {}, ocaml-override ? {}, global-override ? {},
+  bundle ? null, job ? null, inNixShell ? null, src ? ./.,
+}@args:
+let auto = fetchGit {
+  url = "https://github.com/coq-community/coq-nix-toolbox.git";
+  ref = "master";
+  rev = import .nix/coq-nix-toolbox.nix;
+};
+in
+import auto ({inherit src;} // args)
diff --git a/elpi/annot.elpi b/elpi/annot.elpi
index ae44c45..e443328 100644
--- a/elpi/annot.elpi
+++ b/elpi/annot.elpi
@@ -1,19 +1,18 @@
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%                            %                                Trocq                                %
-%  _______                   %                       Copyright (C) 2023 MERCE                      %
-% |__   __|                  %                (Mitsubishi Electric R&D Centre Europe)              %
-%    | |_ __ ___   ___ __ _  %                   Cyril Cohen <cyril.cohen@inria.fr>                %
-%    | | '__/ _ \ / __/ _` | %                   Enzo Crance <enzo.crance@inria.fr>                %
-%    | | | | (_) | (_| (_| | %               Assia Mahboubi <assia.mahboubi@inria.fr>              %
-%    |_|_|  \___/ \___\__, | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%                        | | %            This file is distributed under the terms of the          %
-%                        |_| %              GNU Lesser General Public License Version 3            %
-%                            %             (see LICENSE file for the text of the license)          %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-% --------------------------------------------------------------------------------------------------
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                            %                     Trocq                      %
+%  _______                   %            Copyright (C) 2023 MERCE            %
+% |__   __|                  %     (Mitsubishi Electric R&D Centre Europe)    %
+%    | |_ __ ___   ___ __ _  %        Cyril Cohen <cyril.cohen@inria.fr>      %
+%    | | '__/ _ \ / __/ _` | %        Enzo Crance <enzo.crance@inria.fr>      %
+%    | | | | (_) | (_| (_| | %    Assia Mahboubi <assia.mahboubi@inria.fr>    %
+%    |_|_|  \___/ \___\__, | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                        | | %   This file is distributed under the terms of  %
+%                        |_| %   GNU Lesser General Public License Version 3  %
+%                            % (see LICENSE file for the text of the license) %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% -----------------------------------------------------------------------------
 % annotated type theory
-% --------------------------------------------------------------------------------------------------
+% -----------------------------------------------------------------------------
 
 % this allows to easily make sure an application is beta-reduced
 :before "subst-fun:fail"
@@ -23,7 +22,7 @@ coq.subst-fun Args F FArgs :- !, coq.mk-app F Args FArgs.
 % NB: the output type is term because the annotations are encoded directly in Coq
 % see PType in Param.v
 pred term->annot-term i:term, o:term.
-term->annot-term (sort (typ U)) (app [pglobal (const PType) UI, M, N]) :- param.db.ptype PType, !,
+term->annot-term (sort (typ U)) (app [pglobal (const PType) UI, M, N]) :- trocq.db.ptype PType, !,
   coq.univ-instance UI [{coq.univ.variable U}],
   cstr.univ-link _ M N.
 term->annot-term (fun N T F) (fun N T' F') :- !,
@@ -57,7 +56,7 @@ typecheck T ATy :-
 pred sub-type i:term, i:term.
 % SubUniv
 sub-type (app [pglobal (const PType) _, M1, N1]) (app [pglobal (const PType) _, M2, N2]) :-
-  param.db.ptype PType, !,
+  trocq.db.ptype PType, !,
   cstr.univ-link C1 M1 N1,
   cstr.univ-link C2 M2 N2,
   cstr.geq C1 C2.
@@ -79,7 +78,7 @@ sub-type X _ :- coq.error "annot.sub-type:" X.
 % syntactic term equality, taking care of adding annotation equalities in the constraint graph
 pred eq i:term, i:term.
 eq (app [pglobal (const PType) UI, M1, N1]) (app [pglobal (const PType) UI, M2, N2]) :-
-  param.db.ptype PType, !,
+  trocq.db.ptype PType, !,
   cstr.univ-link C1 M1 N1,
   cstr.univ-link C2 M2 N2,
   cstr.eq C1 C2.
@@ -109,7 +108,7 @@ classes T Cs' Out :-
   ).
 
 pred all-classes i:term, o:list param-class.
-all-classes (app [pglobal (const PType) _, M, N]) [C] :- param.db.ptype PType, !,
+all-classes (app [pglobal (const PType) _, M, N]) [C] :- trocq.db.ptype PType, !,
   cstr.univ-link C M N.
 all-classes X Cs :- (X = prod _ T F ; X = fun _ T F), !,
   pi x\ std.append {all-classes T} {all-classes (F x)} Cs.
@@ -119,7 +118,7 @@ all-classes X [] :- (name X ; X = global _ ; X = pglobal _ _), !.
 all-classes X _ :- coq.error "all-classes:" X.
 
 pred out-class i:term, o:option param-class.
-out-class (app [pglobal (const PType) _, M, N]) (some C) :- param.db.ptype PType, !,
+out-class (app [pglobal (const PType) _, M, N]) (some C) :- trocq.db.ptype PType, !,
   cstr.univ-link C M N.
 out-class (prod _ _ F) Out :- !, pi x\ out-class (F x) Out.
 out-class (fun _ _ _) none :- !.
diff --git a/elpi/constraints/constraint-graph.elpi b/elpi/constraints/constraint-graph.elpi
index ef8c386..bdd9f52 100644
--- a/elpi/constraints/constraint-graph.elpi
+++ b/elpi/constraints/constraint-graph.elpi
@@ -1,19 +1,18 @@
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%                            %                                Trocq                                %
-%  _______                   %                       Copyright (C) 2023 MERCE                      %
-% |__   __|                  %                (Mitsubishi Electric R&D Centre Europe)              %
-%    | |_ __ ___   ___ __ _  %                   Cyril Cohen <cyril.cohen@inria.fr>                %
-%    | | '__/ _ \ / __/ _` | %                   Enzo Crance <enzo.crance@inria.fr>                %
-%    | | | | (_) | (_| (_| | %               Assia Mahboubi <assia.mahboubi@inria.fr>              %
-%    |_|_|  \___/ \___\__, | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%                        | | %            This file is distributed under the terms of the          %
-%                        |_| %              GNU Lesser General Public License Version 3            %
-%                            %             (see LICENSE file for the text of the license)          %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-% --------------------------------------------------------------------------------------------------
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                            %                     Trocq                      %
+%  _______                   %            Copyright (C) 2023 MERCE            %
+% |__   __|                  %     (Mitsubishi Electric R&D Centre Europe)    %
+%    | |_ __ ___   ___ __ _  %        Cyril Cohen <cyril.cohen@inria.fr>      %
+%    | | '__/ _ \ / __/ _` | %        Enzo Crance <enzo.crance@inria.fr>      %
+%    | | | | (_) | (_| (_| | %    Assia Mahboubi <assia.mahboubi@inria.fr>    %
+%    |_|_|  \___/ \___\__, | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                        | | %   This file is distributed under the terms of  %
+%                        |_| %   GNU Lesser General Public License Version 3  %
+%                            % (see LICENSE file for the text of the license) %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% -----------------------------------------------------------------------------
 % definition of the constraint graph
-% --------------------------------------------------------------------------------------------------
+% -----------------------------------------------------------------------------
 
 % in the constraint graph, parametricity classes are represented with integers (it is easier to
 % index on this type than on variables of type param-class)
@@ -160,7 +159,7 @@ instantiate.aux ID Class (node.var (ct.gref GR T GR' GRR) IDs) G G' :-
       G1,
   annot.classes T TCs _,
   % find the output constant and proof, as well as the required classes Cs
-  param.db.gref GR Class Cs GR' GRR,
+  trocq.db.gref GR Class Cs GR' GRR,
   % make sure the classes are consistent
   instantiate.gref IDs TCs Cs G1 G'.
 pred instantiate.gref
diff --git a/elpi/constraints/constraints.elpi b/elpi/constraints/constraints.elpi
index d0d488c..896563d 100644
--- a/elpi/constraints/constraints.elpi
+++ b/elpi/constraints/constraints.elpi
@@ -1,19 +1,18 @@
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%                            %                                Trocq                                %
-%  _______                   %                       Copyright (C) 2023 MERCE                      %
-% |__   __|                  %                (Mitsubishi Electric R&D Centre Europe)              %
-%    | |_ __ ___   ___ __ _  %                   Cyril Cohen <cyril.cohen@inria.fr>                %
-%    | | '__/ _ \ / __/ _` | %                   Enzo Crance <enzo.crance@inria.fr>                %
-%    | | | | (_) | (_| (_| | %               Assia Mahboubi <assia.mahboubi@inria.fr>              %
-%    |_|_|  \___/ \___\__, | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%                        | | %            This file is distributed under the terms of the          %
-%                        |_| %              GNU Lesser General Public License Version 3            %
-%                            %             (see LICENSE file for the text of the license)          %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-% --------------------------------------------------------------------------------------------------
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                            %                     Trocq                      %
+%  _______                   %            Copyright (C) 2023 MERCE            %
+% |__   __|                  %     (Mitsubishi Electric R&D Centre Europe)    %
+%    | |_ __ ___   ___ __ _  %        Cyril Cohen <cyril.cohen@inria.fr>      %
+%    | | '__/ _ \ / __/ _` | %        Enzo Crance <enzo.crance@inria.fr>      %
+%    | | | | (_) | (_| (_| | %    Assia Mahboubi <assia.mahboubi@inria.fr>    %
+%    |_|_|  \___/ \___\__, | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                        | | %   This file is distributed under the terms of  %
+%                        |_| %   GNU Lesser General Public License Version 3  %
+%                            % (see LICENSE file for the text of the license) %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% -----------------------------------------------------------------------------
 % API accessible to the rest of the plugin to handle the constraint graph
-% --------------------------------------------------------------------------------------------------
+% -----------------------------------------------------------------------------
 
 typeabbrev class-id int.
 
@@ -35,7 +34,7 @@ univ-link (pc M' N') M N :-
   map-class->term M' M,
   map-class->term N' N.
 
-% D_π(C) = (C_A, C_B)
+% D_π(C, C_A, C_B)
 pred dep-pi i:param-class, o:param-class, o:param-class.
 dep-pi C CA CB :- var C, !,
   internal.link? C ID,
@@ -45,7 +44,7 @@ dep-pi C CA CB :- var C, !,
 dep-pi C CA CB :-
   param-class.dep-pi C CA CB.
 
-% D_->(C) = (C_A, C_B)
+% D_->(C, C_A, C_B)
 pred dep-arrow i:param-class, o:param-class, o:param-class.
 dep-arrow C CA CB :- var C, !,
   internal.link? C ID,
@@ -65,7 +64,7 @@ dep-type C CR :-
   util.when (param-class.requires-axiom C)
     (geq CR (pc map4 map4)).
 
-% D_K(T)
+% D_K(C, C_1, ..., C_n)
 pred dep-gref i:gref, i:term, o:gref, o:gref.
 dep-gref GR T GR' GRR :-
   annot.classes T TCs OutOpt,
@@ -75,7 +74,7 @@ dep-gref GR T GR' GRR :-
     std.map TCs internal.link? IDs,
     declare_constraint (internal.c.dep-gref ID GR T GR' GRR IDs) [_]
   ) (
-    param.db.gref GR Out Cs GR' GRR,
+    trocq.db.gref GR Out Cs GR' GRR,
     std.forall2 TCs Cs eq
   ).
 
diff --git a/elpi/constraints/simple-graph.elpi b/elpi/constraints/simple-graph.elpi
index e615d2b..1dd3767 100644
--- a/elpi/constraints/simple-graph.elpi
+++ b/elpi/constraints/simple-graph.elpi
@@ -1,19 +1,18 @@
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%                            %                                Trocq                                %
-%  _______                   %                       Copyright (C) 2023 MERCE                      %
-% |__   __|                  %                (Mitsubishi Electric R&D Centre Europe)              %
-%    | |_ __ ___   ___ __ _  %                   Cyril Cohen <cyril.cohen@inria.fr>                %
-%    | | '__/ _ \ / __/ _` | %                   Enzo Crance <enzo.crance@inria.fr>                %
-%    | | | | (_) | (_| (_| | %               Assia Mahboubi <assia.mahboubi@inria.fr>              %
-%    |_|_|  \___/ \___\__, | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%                        | | %            This file is distributed under the terms of the          %
-%                        |_| %              GNU Lesser General Public License Version 3            %
-%                            %             (see LICENSE file for the text of the license)          %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-% --------------------------------------------------------------------------------------------------
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                            %                     Trocq                      %
+%  _______                   %            Copyright (C) 2023 MERCE            %
+% |__   __|                  %     (Mitsubishi Electric R&D Centre Europe)    %
+%    | |_ __ ___   ___ __ _  %        Cyril Cohen <cyril.cohen@inria.fr>      %
+%    | | '__/ _ \ / __/ _` | %        Enzo Crance <enzo.crance@inria.fr>      %
+%    | | | | (_) | (_| (_| | %    Assia Mahboubi <assia.mahboubi@inria.fr>    %
+%    |_|_|  \___/ \___\__, | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                        | | %   This file is distributed under the terms of  %
+%                        |_| %   GNU Lesser General Public License Version 3  %
+%                            % (see LICENSE file for the text of the license) %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% -----------------------------------------------------------------------------
 % definition of a directed graph with no annotation on edges
-% --------------------------------------------------------------------------------------------------
+% -----------------------------------------------------------------------------
 
 kind simple-graph type -> type.
 type simple-graph std.map A (list A) -> simple-graph A.
diff --git a/elpi/param-class.elpi b/elpi/param-class.elpi
index 1398cfe..c76d9fa 100644
--- a/elpi/param-class.elpi
+++ b/elpi/param-class.elpi
@@ -1,19 +1,18 @@
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%                            %                                Trocq                                %
-%  _______                   %                       Copyright (C) 2023 MERCE                      %
-% |__   __|                  %                (Mitsubishi Electric R&D Centre Europe)              %
-%    | |_ __ ___   ___ __ _  %                   Cyril Cohen <cyril.cohen@inria.fr>                %
-%    | | '__/ _ \ / __/ _` | %                   Enzo Crance <enzo.crance@inria.fr>                %
-%    | | | | (_) | (_| (_| | %               Assia Mahboubi <assia.mahboubi@inria.fr>              %
-%    |_|_|  \___/ \___\__, | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%                        | | %            This file is distributed under the terms of the          %
-%                        |_| %              GNU Lesser General Public License Version 3            %
-%                            %             (see LICENSE file for the text of the license)          %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-% --------------------------------------------------------------------------------------------------
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                            %                     Trocq                      %
+%  _______                   %            Copyright (C) 2023 MERCE            %
+% |__   __|                  %     (Mitsubishi Electric R&D Centre Europe)    %
+%    | |_ __ ___   ___ __ _  %        Cyril Cohen <cyril.cohen@inria.fr>      %
+%    | | '__/ _ \ / __/ _` | %        Enzo Crance <enzo.crance@inria.fr>      %
+%    | | | | (_) | (_| (_| | %    Assia Mahboubi <assia.mahboubi@inria.fr>    %
+%    |_|_|  \___/ \___\__, | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                        | | %   This file is distributed under the terms of  %
+%                        |_| %   GNU Lesser General Public License Version 3  %
+%                            % (see LICENSE file for the text of the license) %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% -----------------------------------------------------------------------------
 % definition of parametricity classes
-% --------------------------------------------------------------------------------------------------
+% -----------------------------------------------------------------------------
 
 % a parametricity class is a pair of map classes (levels in our hierarchy)
 kind map-class type.
@@ -177,6 +176,10 @@ dep-arrow map4  (pc map0 map4)  (pc map4 map0).
 
 } % map-class
 
+pred do-not-fail.
+:before "term->gref:fail"
+coq.term->gref _ _ :- do-not-fail, !, false.
+
 namespace param-class {
 
 % extensions of functions over map classes to parametricity classes
@@ -250,4 +253,36 @@ forget (pc M N) (pc M' N') ForgetF :-
 pred requires-axiom i:param-class.
 requires-axiom (pc M N) :- (std.mem! [map2b, map3, map4] M ; std.mem! [map2b, map3, map4] N).
 
+pred type->class i:term, o:list param-class, o:list term.
+type->class X [Class] Ts :-
+  coq.safe-dest-app X HD Ts,
+  (do-not-fail => coq.term->gref HD GRClass),
+  trocq.db.gref->class GRClass Class.
+type->class X [] Ts :- coq.safe-dest-app X _ Ts.
+type->class _ [] [].
+
+pred type->classes.rec i:term, o:list param-class, o:list param-class.
+type->classes.rec (prod N A B) OutList BLast:- !,
+  @pi-decl N A x\
+    type->classes.rec A AList ALast, !,
+    type->classes.rec (B x) BList BLast, !,
+    std.append {std.append AList ALast} BList OutList.
+type->classes.rec X [] Class :- !, type->class X Class _.
+
+pred type->classes.main i:term, o:list param-class, o:list param-class, o:gref, o:gref.
+type->classes.main (prod N A B) OutList BLast GR GR' :- !,
+  @pi-decl N A x\
+    type->classes.rec A AList ALast, !,
+    type->classes.main (B x) BList BLast GR GR', !,
+    std.append {std.append AList ALast} BList OutList.
+type->classes.main X [] Class GR GR' :- !,
+    type->class X Class Ts, !,
+    std.rev Ts [T', T | _],
+    coq.term->gref T GR, coq.term->gref T' GR'.
+
+pred type->classes i:term, o:param-class, o:list param-class, o:gref, o:gref.
+type->classes T OutClass DepClasses GR GR' :-
+  type->classes.main T DepClasses LastClass GR GR',
+  if (LastClass = [OutClass]) true (OutClass = pc map0 map0).
+
 } % param-class
diff --git a/elpi/param.elpi b/elpi/param.elpi
index 9a9ef4e..e6b682d 100644
--- a/elpi/param.elpi
+++ b/elpi/param.elpi
@@ -1,19 +1,19 @@
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%                            %                                Trocq                                %
-%  _______                   %                       Copyright (C) 2023 MERCE                      %
-% |__   __|                  %                (Mitsubishi Electric R&D Centre Europe)              %
-%    | |_ __ ___   ___ __ _  %                   Cyril Cohen <cyril.cohen@inria.fr>                %
-%    | | '__/ _ \ / __/ _` | %                   Enzo Crance <enzo.crance@inria.fr>                %
-%    | | | | (_) | (_| (_| | %               Assia Mahboubi <assia.mahboubi@inria.fr>              %
-%    |_|_|  \___/ \___\__, | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%                        | | %            This file is distributed under the terms of the          %
-%                        |_| %              GNU Lesser General Public License Version 3            %
-%                            %             (see LICENSE file for the text of the license)          %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                            %                     Trocq                      %
+%  _______                   %            Copyright (C) 2023 MERCE            %
+% |__   __|                  %     (Mitsubishi Electric R&D Centre Europe)    %
+%    | |_ __ ___   ___ __ _  %        Cyril Cohen <cyril.cohen@inria.fr>      %
+%    | | '__/ _ \ / __/ _` | %        Enzo Crance <enzo.crance@inria.fr>      %
+%    | | | | (_) | (_| (_| | %    Assia Mahboubi <assia.mahboubi@inria.fr>    %
+%    |_|_|  \___/ \___\__, | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                        | | %   This file is distributed under the terms of  %
+%                        |_| %   GNU Lesser General Public License Version 3  %
+%                            % (see LICENSE file for the text of the license) %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-% --------------------------------------------------------------------------------------------------
+% -----------------------------------------------------------------------------
 % parametricity translation
-% --------------------------------------------------------------------------------------------------
+% -----------------------------------------------------------------------------
 
 :before "subst-fun:fail"
 coq.subst-fun Args F FArgs :- !, coq.mk-app F Args FArgs.
@@ -74,7 +74,7 @@ param X T' X' (W XR) :- name X, !,
 % ParamUniv
 param
   (app [pglobal (const PType) UI, MR, NR] as Type) (app [pglobal (const PType) _, M, N])
-  Type (app [pglobal (const PParamType) UI1|Args]) :- param.db.ptype PType, !, std.do! [
+  Type (app [pglobal (const PParamType) UI1|Args]) :- trocq.db.ptype PType, !, std.do! [
     util.when-debug dbg.steps (coq.say "param/type" MR NR "@" M N),
     cstr.univ-link CR MR NR,
     util.when-debug dbg.full (coq.say "param/type:" MR NR "is linked to" CR),
@@ -85,12 +85,12 @@ param
     coq.univ-instance UI [L],
     coq.univ.variable U L,
     coq.univ-instance UI1 [L, {coq.univ.variable {coq.univ.super U}}], % {coq.univ.new}
-    param.db.pparam-type C PParamType,
+    trocq.db.pparam-type C PParamType,
     util.when-debug dbg.full (coq.say "param/type: suspending proof on" C),
     util.if-suspend C (param-class.requires-axiom C) (
       util.when-debug dbg.full (coq.say "param/type: resuming proof on" C "(univalence needed)"),
       coq.univ-instance UI0 [],
-      Args = [MR, NR, pglobal (const {param.db.univalence}) UI0]
+      Args = [MR, NR, pglobal (const {trocq.db.univalence}) UI0]
     ) (
       util.when-debug dbg.full
         (coq.say "param/type: resuming proof on" C "(univalence not needed)"),
@@ -106,14 +106,14 @@ param (fun N T F) FunTy (fun N' T' F') FunR :- !,
   coq.name-suffix N "'" N',
   coq.name-suffix N "R" NR,
   map-class->term map0 Map0,
-  param T (app [pglobal (const {param.db.ptype}) _, Map0, Map0]) T' TR,
+  param T (app [pglobal (const {trocq.db.ptype}) _, Map0, Map0]) T' TR,
   util.when-debug dbg.full (coq.say "param/fun:" T "@ 0,0 ~" T' "by" TR),
   @annot-pi-decl N T x\ pi x' xR\ param.store x T x' xR => (
     util.when-debug dbg.full (coq.say "param/fun: introducing" x "@" T "~" x' "by" xR),
     param (F x) (TF x) (F' x') (FR x x' xR),
     util.when-debug dbg.full (coq.say "param/fun:" (F x) "@" (TF x) "~" (F' x') "by" (FR x x' xR))
   ),
-  param.db.r (pc map0 map0) R,
+  trocq.db.r (pc map0 map0) R,
   prune UI [],
   FunR =
     fun N T x\ fun N' T' x'\ fun NR (app [pglobal (const R) UI, T, T', TR, x, x']) xR\ FR x x' xR.
@@ -122,7 +122,7 @@ param (fun N T F) FunTy (fun N' T' F') FunR :- !,
 param
   (prod _ A (_\ B)) (app [pglobal (const PType) _, M, N])
   (prod `_` A' (_\ B')) (app [pglobal (const ParamArrow) UI|Args]) :-
-    param.db.ptype PType, !, std.do! [
+    trocq.db.ptype PType, !, std.do! [
       util.when-debug dbg.steps (coq.say "param/arrow" A "->" B "@" M N),
       cstr.univ-link C M N,
       util.when-debug dbg.full (coq.say "param/arrow:" M N "is linked to" C),
@@ -136,14 +136,14 @@ param
       param B (app [pglobal (const PType) _, MB, NB]) B' BR,
       util.when-debug dbg.full (coq.say "param/arrow:" B "@" MB NB "~" B' "by" BR),
       coq.say "before db param-arrow" C,
-      param.db.param-arrow C ParamArrow,
+      trocq.db.param-arrow C ParamArrow,
       coq.say UI,
       prune UI [],
       util.when-debug dbg.full (coq.say "param/arrow: suspending proof on" C),
       util.if-suspend C (param-class.requires-axiom C) (
         util.when-debug dbg.full (coq.say "param/arrow: resuming proof on" C "(funext needed)"),
         coq.univ-instance UI0 [],
-        Args = [pglobal (const {param.db.funext}) UI0, A, A', AR, B, B', BR]
+        Args = [pglobal (const {trocq.db.funext}) UI0, A, A', AR, B, B', BR]
       ) (
         util.when-debug dbg.full (coq.say "param/arrow: resuming proof on" C "(funext not needed)"),
         Args = [A, A', AR, B, B', BR]
@@ -153,7 +153,7 @@ param
 % ParamPi
 param
   (prod N A B) (app [pglobal (const PType) _, M1, M2])
-  (prod N' A' B') (app [pglobal (const ParamForall) UI|Args']) :- param.db.ptype PType, !,
+  (prod N' A' B') (app [pglobal (const ParamForall) UI|Args']) :- trocq.db.ptype PType, !,
     util.when-debug dbg.steps (coq.say "param/forall" N ":" A "," B "@" M1 M2),
     coq.name-suffix N "'" N',
     coq.name-suffix N "R" NR,
@@ -171,19 +171,19 @@ param
       param (B a) (app [pglobal (const PType) _, M1B, M2B]) (B' a') (BR a a' aR),
       util.when-debug dbg.full (coq.say "param/forall:" (B a) "@" M1B M2B "~" (B' a') "by" (BR a a' aR))
     ),
-    param.db.r CA RA,
+    trocq.db.r CA RA,
     prune UIA [],
     Args =
       [ A, A', AR, fun N A B, fun N' A' B',
         fun N A a\ fun N' A' a'\ fun NR (app [pglobal (const RA) UIA, A, A', AR, a, a']) aR\
           BR a a' aR ],
-    param.db.param-forall C ParamForall,
+    trocq.db.param-forall C ParamForall,
     prune UI [],
     util.when-debug dbg.full (coq.say "param/forall: suspending proof on" C),
     util.if-suspend C (param-class.requires-axiom C) (
       util.when-debug dbg.full (coq.say "param/forall: resuming proof on" C "(funext needed)"),
       coq.univ-instance UI0 [],
-      Args' = [pglobal (const {param.db.funext}) UI0|Args]
+      Args' = [pglobal (const {trocq.db.funext}) UI0|Args]
     ) (
       util.when-debug dbg.full (coq.say "param/forall: resuming proof on" C "(funext not needed)"),
       Args' = Args
@@ -221,8 +221,8 @@ type wsuspend (term -> term) -> (term -> term) -> weakening.
 % generate the weakening function from a type to a sub-type
 pred weakening i:term, i:term, o:weakening.
 weakening (app [pglobal (const PType) _, M, N]) (app [pglobal (const PType) _, M', N']) W :-
-  param.db.ptype PType, !,
-  param.db.weaken Weaken,
+  trocq.db.ptype PType, !,
+  trocq.db.weaken Weaken,
   prune UI [],
   prune Ty [],
   % as M, N, M', N' are not known yet, we put a Coq placeholder (see Weaken in Param.v)
@@ -247,7 +247,7 @@ weakening T _ _ :- coq.error "weakening:" T.
 % replace Weaken placeholders with real weakening functions
 pred param.subst-weaken i:term, o:term.
 param.subst-weaken T T' :-
-  param.db.weaken Weaken,
+  trocq.db.weaken Weaken,
   (pi XR XR'\ copy (app [pglobal (const Weaken) _, _, _, _, _, _, _] as XR) XR' :- !,
     copy.subst-weaken XR XR')
       => copy T T'.
diff --git a/elpi/util.elpi b/elpi/util.elpi
index 6eee5b8..2141a24 100644
--- a/elpi/util.elpi
+++ b/elpi/util.elpi
@@ -1,19 +1,18 @@
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%                            %                                Trocq                                %
-%  _______                   %                       Copyright (C) 2023 MERCE                      %
-% |__   __|                  %                (Mitsubishi Electric R&D Centre Europe)              %
-%    | |_ __ ___   ___ __ _  %                   Cyril Cohen <cyril.cohen@inria.fr>                %
-%    | | '__/ _ \ / __/ _` | %                   Enzo Crance <enzo.crance@inria.fr>                %
-%    | | | | (_) | (_| (_| | %               Assia Mahboubi <assia.mahboubi@inria.fr>              %
-%    |_|_|  \___/ \___\__, | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%                        | | %            This file is distributed under the terms of the          %
-%                        |_| %              GNU Lesser General Public License Version 3            %
-%                            %             (see LICENSE file for the text of the license)          %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-% --------------------------------------------------------------------------------------------------
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                            %                     Trocq                      %
+%  _______                   %            Copyright (C) 2023 MERCE            %
+% |__   __|                  %     (Mitsubishi Electric R&D Centre Europe)    %
+%    | |_ __ ___   ___ __ _  %        Cyril Cohen <cyril.cohen@inria.fr>      %
+%    | | '__/ _ \ / __/ _` | %        Enzo Crance <enzo.crance@inria.fr>      %
+%    | | | | (_) | (_| (_| | %    Assia Mahboubi <assia.mahboubi@inria.fr>    %
+%    |_|_|  \___/ \___\__, | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                        | | %   This file is distributed under the terms of  %
+%                        |_| %   GNU Lesser General Public License Version 3  %
+%                            % (see LICENSE file for the text of the license) %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% -----------------------------------------------------------------------------
 % utility predicates
-% --------------------------------------------------------------------------------------------------
+% -----------------------------------------------------------------------------
 
 kind or type -> type -> type.
 type inl A -> or A B.
diff --git a/examples/Example.v b/examples/Example.v
index e20ba17..28fc1e8 100644
--- a/examples/Example.v
+++ b/examples/Example.v
@@ -1,15 +1,15 @@
-(**************************************************************************************************)
-(*                            *                               Trocq                               *)
-(*  _______                   *                      Copyright (C) 2023 MERCE                     *)
-(* |__   __|                  *               (Mitsubishi Electric R&D Centre Europe)             *)
-(*    | |_ __ ___   ___ __ _  *                  Cyril Cohen <cyril.cohen@inria.fr>               *)
-(*    | | '__/ _ \ / __/ _` | *                  Enzo Crance <enzo.crance@inria.fr>               *)
-(*    | | | | (_) | (_| (_| | *              Assia Mahboubi <assia.mahboubi@inria.fr>             *)
-(*    |_|_|  \___/ \___\__, | *********************************************************************)
-(*                        | | *           This file is distributed under the terms of the         *)
-(*                        |_| *             GNU Lesser General Public License Version 3           *)
-(*                            *            (see LICENSE file for the text of the license)         *)
-(**************************************************************************************************)
+(*****************************************************************************)
+(*                            *                    Trocq                     *)
+(*  _______                   *           Copyright (C) 2023 MERCE           *)
+(* |__   __|                  *    (Mitsubishi Electric R&D Centre Europe)   *)
+(*    | |_ __ ___   ___ __ _  *       Cyril Cohen <cyril.cohen@inria.fr>     *)
+(*    | | '__/ _ \ / __/ _` | *       Enzo Crance <enzo.crance@inria.fr>     *)
+(*    | | | | (_) | (_| (_| | *   Assia Mahboubi <assia.mahboubi@inria.fr>   *)
+(*    |_|_|  \___/ \___\__, | ************************************************)
+(*                        | | * This file is distributed under the terms of  *)
+(*                        |_| * GNU Lesser General Public License Version 3  *)
+(*                            * see LICENSE file for the text of the license *)
+(*****************************************************************************)
 
 From elpi Require Import elpi.
 From Coq Require Import ssreflect.
@@ -25,8 +25,8 @@ Set Universe Polymorphism.
 Axiom u : Univalence.
 Axiom f : Funext.
 
-Param Register Univalence u.
-Param Register Funext f.
+Trocq Register Univalence u.
+Trocq Register Funext f.
 
 Goal
   (* Type@{i}. *)
diff --git a/examples/int_to_Zp.v b/examples/int_to_Zp.v
index fe8153d..3683c51 100644
--- a/examples/int_to_Zp.v
+++ b/examples/int_to_Zp.v
@@ -1,18 +1,17 @@
-(**************************************************************************************************)
-(*                            *                               Trocq                               *)
-(*  _______                   *                      Copyright (C) 2023 MERCE                     *)
-(* |__   __|                  *               (Mitsubishi Electric R&D Centre Europe)             *)
-(*    | |_ __ ___   ___ __ _  *                  Cyril Cohen <cyril.cohen@inria.fr>               *)
-(*    | | '__/ _ \ / __/ _` | *                  Enzo Crance <enzo.crance@inria.fr>               *)
-(*    | | | | (_) | (_| (_| | *              Assia Mahboubi <assia.mahboubi@inria.fr>             *)
-(*    |_|_|  \___/ \___\__, | *********************************************************************)
-(*                        | | *           This file is distributed under the terms of the         *)
-(*                        |_| *             GNU Lesser General Public License Version 3           *)
-(*                            *            (see LICENSE file for the text of the license)         *)
-(**************************************************************************************************)
+(*****************************************************************************)
+(*                            *                    Trocq                     *)
+(*  _______                   *           Copyright (C) 2023 MERCE           *)
+(* |__   __|                  *    (Mitsubishi Electric R&D Centre Europe)   *)
+(*    | |_ __ ___   ___ __ _  *       Cyril Cohen <cyril.cohen@inria.fr>     *)
+(*    | | '__/ _ \ / __/ _` | *       Enzo Crance <enzo.crance@inria.fr>     *)
+(*    | | | | (_) | (_| (_| | *   Assia Mahboubi <assia.mahboubi@inria.fr>   *)
+(*    |_|_|  \___/ \___\__, | ************************************************)
+(*                        | | * This file is distributed under the terms of  *)
+(*                        |_| * GNU Lesser General Public License Version 3  *)
+(*                            * see LICENSE file for the text of the license *)
+(*****************************************************************************)
 
 From Coq Require Import ssreflect.
-From HoTT Require Import HoTT.
 From Trocq Require Import Trocq.
 
 Set Universe Polymorphism.
@@ -73,72 +72,28 @@ Proof. apply addp_to_add. Qed.
 
 Check Param01_paths.
 
-Elpi Query param lp:{{
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref Zp}} (pc map4 map2b) [] {{:gref int}} {{:gref Rp42b}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref Zp}} (pc map4 map0) [] {{:gref int}} {{:gref Rp40}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref Zp}} (pc map0 map0) [] {{:gref int}} {{:gref Rp00}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref Zp}} (pc map0 map1) [] {{:gref int}} {{:gref Rp01}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref Zp}} (pc map1 map0) [] {{:gref int}} {{:gref Rp10}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref Zp}} (pc map0 map2b) [] {{:gref int}} {{:gref Rp02b}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref Zp}} (pc map2b map0) [] {{:gref int}} {{:gref Rp2b0}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref Zp}} (pc map2a map0) [] {{:gref int}} {{:gref Rp2a0}})),
-  
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref
-        {{:gref paths}} (pc map0 map1)
-        [pc map0 map2b]
-        {{:gref paths}} {{:gref Param01_paths}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref
-        {{:gref paths}} (pc map1 map0)
-        [pc map2b map0]
-        {{:gref paths}} {{:gref Param10_paths}})),
+Trocq Use Rp42b.
+Trocq Use Rp40.
+Trocq Use Rp00.
+Trocq Use Rp01.
+Trocq Use Rp10.
+Trocq Use Rp02b.
+Trocq Use Rp2b0.
+Trocq Use Rp2a0.
 
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref addp}} (pc map0 map0) [] {{:gref add}} {{:gref Radd}})).
-}}.
+Trocq Use Param01_paths.
+Trocq Use Param10_paths.
+Trocq Use Radd.
 
 Axiom u : Univalence.
 Axiom f : Funext.
 
-Param Register Univalence u.
-Param Register Funext f.
+Trocq Register Univalence u.
+Trocq Register Funext f.
 
-Goal
-  (* Zp@{i}. *)
-  (* Zp@{i} -> Zp@{i}. *)
-  (* forall (P : Zp -> Type) (x : Zp), P x. *)
-  (* forall (P : Zp -> Type) (x : Zp), P x -> P x. *)
-  (* forall (P : Zp -> Zp -> Type) (x y : Zp), P x y -> P y x. *)
-  (* forall (P : Zp -> Type) (x : Zp), P x -> forall (y : Zp), P y. *)
-  (* forall (P : Zp -> Type) (x : Zp), P x -> forall (y : Zp), P y -> P x. *)
-  (* forall (A : Type) (f : Zp -> A) (P : A -> Type) (x : Zp), P (f x). *)
-  (* forall (A : Type) (f : Zp -> A) (P : A -> Type) (x : Zp) (H : forall a, P a -> Type) (J : P (f x)), H (f x) J. *)
-
-  (forall x y, x + y = y + x)%Zp.
-
-  (* forall (X : forall (A : Type@{i}), A -> Type@{i}) (x : Zp), Zp -> X Zp x -> Zp. *)
+Goal (forall x y, x + y = y + x)%Zp.
 Proof.
-  param.
+  trocq.
 Abort.
 
 Goal (forall x y, x + y = y + x)%int ->
@@ -147,202 +102,6 @@ Proof.
   intros addC x y z.
   suff addpC: forall x y, (x + y = y + x)%Zp. {
     by rewrite (addpC x y). }
-  param.
+  trocq.
   exact addC.
 Qed.
-
-Inductive unit@{i} : Type@{i} := tt : unit.
-
-Module Seq.
-  Inductive t@{i} (A : Type@{i}) :=
-    | snil : t A
-    | scons : A -> (unit@{i} -> t A) -> t A.
-  Arguments snil {_}.
-  Arguments scons {_} _ _.
-  
-  Fixpoint all@{i} {A : Type@{i}} (P : A -> Type@{i}) (s : t A) : Type@{i} :=
-    match s with
-    | snil => unit@{i}
-    | scons a s' => P a * all P (s' tt)
-    end.
-
-  Fixpoint sum@{i} (s : t Zp) : Zp :=
-    match s with
-    | snil => zerop@{i}
-    | scons x s' => (x + sum (s' tt))%Zp
-    end.
-End Seq.
-
-Fixpoint all@{i} {A : Type@{i}} (P : A -> Type@{i}) (l : list A) : Type@{i} :=
-  match l with
-  | nil => unit@{i}
-  | cons a l' => P a * all P l'
-  end.
-
-Definition sum@{i} (l : list@{i} int) : int := List.fold_left@{i i} _ _ add@{i} l zero.
-
-Inductive Rseq@{i}
-  (A A' : Type@{i}) (AR : A -> A' -> Type@{i}) : Seq.t@{i} A -> list@{i} A' -> Type@{i} :=
-    | Rnil : Rseq A A' AR Seq.snil nil
-    | Rcons : forall a a' (aR : AR a a') s l (r : Rseq A A' AR s l),
-      Rseq A A' AR (Seq.scons a (fun _ => s)) (cons a' l).
-
-Fixpoint map_seq@{i} (A A' : Type@{i}) (AR : Param10.Rel A A') (s : Seq.t@{i} A) : list@{i} A' :=
-  match s with
-  | Seq.snil => nil
-  | Seq.scons a s' => cons (map AR a) (map_seq A A' AR (s' tt))
-  end.
-
-Definition Param2a0_seq_list@{i} (A A' : Type@{i}) (AR : Param2a0.Rel A A') :
-  Param2a0.Rel (Seq.t A) (list A').
-Proof.
-  unshelve econstructor.
-  - exact (Rseq A A' AR).
-  - apply cheat@{i}.
-  - apply cheat@{i}.
-Defined.
-
-Definition Param02b_seq_list@{i} (A A' : Type@{i}) (AR : Param02b.Rel A A') :
-  Param02b.Rel (Seq.t A) (list A').
-Proof.
-  unshelve econstructor.
-  - exact (Rseq A A' AR).
-  - apply cheat@{i}.
-  - apply cheat@{i}.
-Defined.
-
-Definition Param44_seq_list@{i} (A A' : Type@{i}) (AR : Param44.Rel A A') :
-  Param44.Rel (Seq.t A) (list A').
-Proof.
-  unshelve econstructor.
-  - exact (Rseq A A' AR).
-  - apply cheat@{i}.
-  - apply cheat@{i}.
-Defined.
-
-(* Definition Param01_seq_list@{i} :
-  forall (A A' : Type@{i}) (AR : Param01.Rel A A'), Param01.Rel (Seq.t A) (list A').
-Proof.
-  intros A A' AR.
-  unshelve econstructor.
-  - exact (Rseq A A' AR).
-  - constructor.
-  - cheat.
-Defined. *)
-
-Fixpoint Rall01@{i}
-  (A A' : Type@{i}) (AR : Param00.Rel A A')
-  (P : A -> Type@{i}) (P' : A' -> Type@{i})
-  (PR : forall a a' (aR : AR a a'), Param01.Rel (P a) (P' a'))
-  (s : Seq.t A) (l : list A') (slR : Rseq A A' AR s l) :
-    Param01.Rel (Seq.all P s) (all P' l).
-Proof.
-  unshelve econstructor.
-  - destruct slR.
-    + simpl. exact (fun _ _ => unit@{i}).
-    + simpl. intros (pa, ps) (pa', pl).
-      exact (PR a a' aR pa pa' * Rall01 A A' AR P P' PR s l slR ps pl).
-  - constructor.
-  - unshelve econstructor.
-    destruct slR.
-    + simpl. exact (fun u => u).
-    + simpl. intros (pa', pl).
-      exact (comap (PR a a' aR) pa', comap (Rall01 A A' AR P P' PR s l slR) pl).
-Defined.
-
-Fixpoint Rall10@{i}
-  (A A' : Type@{i}) (AR : Param00.Rel A A')
-  (P : A -> Type@{i}) (P' : A' -> Type@{i})
-  (PR : forall a a' (aR : AR a a'), Param10.Rel (P a) (P' a'))
-  (s : Seq.t A) (l : list A') (slR : Rseq A A' AR s l) :
-    Param10.Rel (Seq.all P s) (all P' l).
-Proof.
-  unshelve econstructor.
-  - destruct slR.
-    + simpl. exact (fun _ _ => unit@{i}).
-    + simpl. intros (pa, ps) (pa', pl).
-      exact (PR a a' aR pa pa' * Rall10 A A' AR P P' PR s l slR ps pl).
-  - unshelve econstructor.
-    destruct slR.
-    + simpl. exact (fun u => u).
-    + simpl. intros (pa, ps).
-      exact (map (PR a a' aR) pa, map (Rall10 A A' AR P P' PR s l slR) ps).
-  - constructor.
-Defined.
-
-Definition Rsum :
-  forall (s : Seq.t Zp) (l : list int) (slR : Rseq Zp int Rp00 s l),
-    Rp00 (Seq.sum s) (sum l).
-Admitted.
-
-Axiom Rzero : Rp zerop zero.
-
-Definition Rp02a : Param02a.Rel Zp int.
-Proof.
-  unshelve econstructor.
-  - exact Rp.
-  - constructor.
-  - cheat.
-Defined.
-
-Elpi Query param lp:{{
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref Zp}} (pc map0 map2a) [] {{:gref int}} {{:gref Rp02a}})),
-
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref
-        {{:gref Seq.t}} (pc map2a map0)
-        [pc map2a map0]
-        {{:gref list}} {{:gref Param2a0_seq_list}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref
-        {{:gref Seq.t}} (pc map4 map4)
-        [pc map4 map4]
-        {{:gref list}} {{:gref Param44_seq_list}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref
-        {{:gref Seq.t}} (pc map0 map2b)
-        [pc map0 map2b]
-        {{:gref list}} {{:gref Param02b_seq_list}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref
-        {{:gref Seq.all}} (pc map0 map1)
-        [pc map0 map0, pc map0 map1]
-        {{:gref all}} {{:gref Rall01}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref
-        {{:gref Seq.all}} (pc map1 map0)
-        [pc map0 map0, pc map1 map0]
-        {{:gref all}} {{:gref Rall10}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref
-        {{:gref Seq.snil}} (pc map0 map0)
-        [pc map0 map0]
-        {{:gref nil}} {{:gref Rnil}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref zerop}} (pc map0 map0) [] {{:gref zero}} {{:gref Rzero}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref Seq.sum}} (pc map0 map0) [] {{:gref sum}} {{:gref Rsum}})).
-}}.
-
-Goal
-  (* forall (s : Seq.t Zp), s = s. *)
-  (* Seq.all (fun x : Zp => Zp) Seq.snil. *)
-  (* forall (s : Seq.t Zp), Seq.all (fun x : Zp => Zp) s. *)
-  (* forall (P : Zp -> Type), Seq.all P Seq.snil. *)
-  (* forall (P : Zp -> Type) (s : Seq.t Zp), Seq.all P s. *)
-  forall (F : (Type@{i} -> Type@{i}) -> Type@{i}), F Seq.t.
-  (* forall (P : Zp -> Type) (s : Seq.t Zp),
-    (forall x, P x -> x = zerop) -> Seq.all P s -> Seq.sum s = zerop. *)
-Proof.
-  param.
-Abort.
diff --git a/examples/peano_bin_nat.v b/examples/peano_bin_nat.v
index 7b83b5e..798c3e6 100644
--- a/examples/peano_bin_nat.v
+++ b/examples/peano_bin_nat.v
@@ -1,15 +1,15 @@
-(**************************************************************************************************)
-(*                            *                               Trocq                               *)
-(*  _______                   *                      Copyright (C) 2023 MERCE                     *)
-(* |__   __|                  *               (Mitsubishi Electric R&D Centre Europe)             *)
-(*    | |_ __ ___   ___ __ _  *                  Cyril Cohen <cyril.cohen@inria.fr>               *)
-(*    | | '__/ _ \ / __/ _` | *                  Enzo Crance <enzo.crance@inria.fr>               *)
-(*    | | | | (_) | (_| (_| | *              Assia Mahboubi <assia.mahboubi@inria.fr>             *)
-(*    |_|_|  \___/ \___\__, | *********************************************************************)
-(*                        | | *           This file is distributed under the terms of the         *)
-(*                        |_| *             GNU Lesser General Public License Version 3           *)
-(*                            *            (see LICENSE file for the text of the license)         *)
-(**************************************************************************************************)
+(*****************************************************************************)
+(*                            *                    Trocq                     *)
+(*  _______                   *           Copyright (C) 2023 MERCE           *)
+(* |__   __|                  *    (Mitsubishi Electric R&D Centre Europe)   *)
+(*    | |_ __ ___   ___ __ _  *       Cyril Cohen <cyril.cohen@inria.fr>     *)
+(*    | | '__/ _ \ / __/ _` | *       Enzo Crance <enzo.crance@inria.fr>     *)
+(*    | | | | (_) | (_| (_| | *   Assia Mahboubi <assia.mahboubi@inria.fr>   *)
+(*    |_|_|  \___/ \___\__, | ************************************************)
+(*                        | | * This file is distributed under the terms of  *)
+(*                        |_| * GNU Lesser General Public License Version 3  *)
+(*                            * see LICENSE file for the text of the license *)
+(*****************************************************************************)
 
 From Coq Require Import ssreflect.
 From HoTT Require Import HoTT.
@@ -131,7 +131,8 @@ Lemma Nmap_in_R@{} (m : N) (n : nat) :
   paths@{Set} (Nmap m) n -> sym_rel@{Set} RN n m.
 Proof. by move<-; apply: NmapK. Qed.
 
-(* the best we can do to link these types is (2a,3) *)
+(* the best we can do to link these types is (4,4), but
+we only need (2a,3) which is morally that Nmap is a split injection *)
 
 Definition RN2a3@{} : Param2a3.Rel@{Set} N nat := @Param2a3.BuildRel@{Set} N nat RN@{}
    (@Map2a.BuildHas@{Set} _ _ _ Nmap Nmap_in_R)
@@ -156,31 +157,16 @@ Definition RN0 : RN N0 0. Proof. done. Qed.
 Definition RNS : forall m n, RN m n -> RN (Nsucc m) (S n).
 Proof. by move=> _ + <-; case=> //=. Qed.
 
-Elpi Query param lp:{{
-  % register Param N nat
-  % as said higher, with some automation this can be turned into only one declaration
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref N}} (pc map0 map2b) [] {{:gref nat}} {{:gref RN02b}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref N}} (pc map0 map2a) [] {{:gref nat}} {{:gref RN02a}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref N}} (pc map2a map0) [] {{:gref nat}} {{:gref RN2a0}})),
-  % register the constants
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref N0}} (pc map0 map0) [] {{:gref O}} {{:gref RN0}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref Nsucc}} (pc map0 map0) [] {{:gref S}} {{:gref RNS}})).
-}}.
+Trocq Use RN02b.
+Trocq Use RN02a.
+Trocq Use RN2a0.
+Trocq Use RN0.
+Trocq Use RNS.
 
 Lemma N_Srec : forall (P : N -> Type), P N0 ->
  (forall n, P n -> P (Nsucc n)) -> forall n, P n.
 Proof.
-  param.
+  trocq.
   (* the output sort of P' is (1,1) because of the covariant and contravariant occurrences of P in
      the input goal; this annotation was made to be definitionally equal to Type: from there,
      the induction principle of nat can be applied directly *)
@@ -188,4 +174,4 @@ Proof.
 Defined.
 
 Print N_Srec.
-Print Assumptions N_Srec.
\ No newline at end of file
+Print Assumptions N_Srec.
diff --git a/examples/setoid_rewrite.v b/examples/setoid_rewrite.v
index 295e475..5d0d14b 100644
--- a/examples/setoid_rewrite.v
+++ b/examples/setoid_rewrite.v
@@ -1,15 +1,15 @@
-(**************************************************************************************************)
-(*                            *                               Trocq                               *)
-(*  _______                   *                      Copyright (C) 2023 MERCE                     *)
-(* |__   __|                  *               (Mitsubishi Electric R&D Centre Europe)             *)
-(*    | |_ __ ___   ___ __ _  *                  Cyril Cohen <cyril.cohen@inria.fr>               *)
-(*    | | '__/ _ \ / __/ _` | *                  Enzo Crance <enzo.crance@inria.fr>               *)
-(*    | | | | (_) | (_| (_| | *              Assia Mahboubi <assia.mahboubi@inria.fr>             *)
-(*    |_|_|  \___/ \___\__, | *********************************************************************)
-(*                        | | *           This file is distributed under the terms of the         *)
-(*                        |_| *             GNU Lesser General Public License Version 3           *)
-(*                            *            (see LICENSE file for the text of the license)         *)
-(**************************************************************************************************)
+(*****************************************************************************)
+(*                            *                    Trocq                     *)
+(*  _______                   *           Copyright (C) 2023 MERCE           *)
+(* |__   __|                  *    (Mitsubishi Electric R&D Centre Europe)   *)
+(*    | |_ __ ___   ___ __ _  *       Cyril Cohen <cyril.cohen@inria.fr>     *)
+(*    | | '__/ _ \ / __/ _` | *       Enzo Crance <enzo.crance@inria.fr>     *)
+(*    | | | | (_) | (_| (_| | *   Assia Mahboubi <assia.mahboubi@inria.fr>   *)
+(*    |_|_|  \___/ \___\__, | ************************************************)
+(*                        | | * This file is distributed under the terms of  *)
+(*                        |_| * GNU Lesser General Public License Version 3  *)
+(*                            * see LICENSE file for the text of the license *)
+(*****************************************************************************)
 
 From Coq Require Import Prelude.
 From Coq Require Import Setoid Morphisms.
diff --git a/examples/summable.v b/examples/summable.v
index c2422be..b208d6d 100644
--- a/examples/summable.v
+++ b/examples/summable.v
@@ -1,15 +1,15 @@
-(**************************************************************************************************)
-(*                            *                               Trocq                               *)
-(*  _______                   *                      Copyright (C) 2023 MERCE                     *)
-(* |__   __|                  *               (Mitsubishi Electric R&D Centre Europe)             *)
-(*    | |_ __ ___   ___ __ _  *                  Cyril Cohen <cyril.cohen@inria.fr>               *)
-(*    | | '__/ _ \ / __/ _` | *                  Enzo Crance <enzo.crance@inria.fr>               *)
-(*    | | | | (_) | (_| (_| | *              Assia Mahboubi <assia.mahboubi@inria.fr>             *)
-(*    |_|_|  \___/ \___\__, | *********************************************************************)
-(*                        | | *           This file is distributed under the terms of the         *)
-(*                        |_| *             GNU Lesser General Public License Version 3           *)
-(*                            *            (see LICENSE file for the text of the license)         *)
-(**************************************************************************************************)
+(*****************************************************************************)
+(*                            *                    Trocq                     *)
+(*  _______                   *           Copyright (C) 2023 MERCE           *)
+(* |__   __|                  *    (Mitsubishi Electric R&D Centre Europe)   *)
+(*    | |_ __ ___   ___ __ _  *       Cyril Cohen <cyril.cohen@inria.fr>     *)
+(*    | | '__/ _ \ / __/ _` | *       Enzo Crance <enzo.crance@inria.fr>     *)
+(*    | | | | (_) | (_| (_| | *   Assia Mahboubi <assia.mahboubi@inria.fr>   *)
+(*    |_|_|  \___/ \___\__, | ************************************************)
+(*                        | | * This file is distributed under the terms of  *)
+(*                        |_| * GNU Lesser General Public License Version 3  *)
+(*                            * see LICENSE file for the text of the license *)
+(*****************************************************************************)
 
 From Coq Require Import ssreflect.
 From HoTT Require Import HoTT.
@@ -19,149 +19,146 @@ Set Universe Polymorphism.
 
 (* first, we axiomatise non negative reals *)
 
-Axiom (nnreal : Type).
-Declare Scope nnreal_scope.
-Delimit Scope nnreal_scope with nnreal.
-Bind Scope nnreal_scope with nnreal.
+Axiom (nnR : Type).
+Declare Scope nnR_scope.
+Delimit Scope nnR_scope with nnR.
+Bind Scope nnR_scope with nnR.
 
-Axiom (nnreal_zero : nnreal).
-Axiom (nnreal_add : nnreal -> nnreal -> nnreal).
-Notation "x + y" := (nnreal_add x%nnreal y%nnreal) : nnreal_scope.
+Axiom (zero_nnR : nnR).
+Notation "0" := zero_nnR : nnR_scope.
+
+Axiom (add_nnR : nnR -> nnR -> nnR).
+Notation "x + y" := (add_nnR x%nnR y%nnR) : nnR_scope.
 
 (* the extension is just defined as adding a constructor for infinite reals *)
 
-Inductive xnnreal : Type :=
-  | Fin : nnreal -> xnnreal
-  | Inf : xnnreal.
+Inductive xnnR : Type :=
+  | Fin : nnR -> xnnR
+  | Inf : xnnR.
 
-Declare Scope xnnreal_scope.
-Delimit Scope xnnreal_scope with xnnreal.
-Bind Scope xnnreal_scope with xnnreal.
+Declare Scope xnnR_scope.
+Delimit Scope xnnR_scope with xnnR.
+Bind Scope xnnR_scope with xnnR.
 
-Definition xnnreal_add (re1 re2 : xnnreal) : xnnreal :=
+Definition add_xnnR (re1 re2 : xnnR) : xnnR :=
   match re1, re2 with
-  | Fin r1, Fin r2 => Fin (r1 + r2)%nnreal
+  | Fin r1, Fin r2 => Fin (r1 + r2)%nnR
   | _, _ => Inf
   end.
-Notation "x + y" := (xnnreal_add x%xnnreal y%xnnreal) : xnnreal_scope.
+Notation "x + y" := (add_xnnR x%xnnR y%xnnR) : xnnR_scope.
 
-Definition xnnreal_seq := nat -> xnnreal.
-Identity Coercion xnnreal_seq_id : xnnreal_seq >-> Funclass.
-Declare Scope xnnreal_seq_scope.
-Delimit Scope xnnreal_seq_scope with xnnreal_seq.
-Bind Scope xnnreal_seq_scope with xnnreal_seq.
+Definition seq_xnnR := nat -> xnnR.
+Identity Coercion seq_xnnR_id : seq_xnnR >-> Funclass.
+Declare Scope seq_xnnR_scope.
+Delimit Scope seq_xnnR_scope with seq_xnnR.
+Bind Scope seq_xnnR_scope with seq_xnnR.
 
-Definition add_xnnreal_seq (u v : xnnreal_seq) : xnnreal_seq :=
-  fun n => (u n + v n)%xnnreal.
-Infix "+" := add_xnnreal_seq : xnnreal_seq_scope.
+Definition add_seq_xnnR (u v : seq_xnnR) : seq_xnnR :=
+  fun n => (u n + v n)%xnnR.
+Infix "+" := add_seq_xnnR : seq_xnnR_scope.
 
-Definition nnreal_seq := nat -> nnreal.
-Identity Coercion nnreal_seq_id : nnreal_seq >-> Funclass.
+Definition seq_nnR := nat -> nnR.
+Identity Coercion seq_nnR_id : seq_nnR >-> Funclass.
 
 (* here we axiomatise the sequence sum and the distributivity lemma *)
-(* TODO: expliquer pourquoi? *)
 
-Axiom (xnnreal_sum : xnnreal_seq -> xnnreal).
-Notation "'Σ' ue" := (xnnreal_sum ue) (at level 35) : xnnreal_scope.
+Axiom (sum_xnnR : seq_xnnR -> xnnR).
+Notation "'Σ' ue" := (sum_xnnR ue) (at level 35) : xnnR_scope.
+
+Axiom sum_xnnR_add :
+  forall u v : seq_xnnR, (Σ (u + v))%xnnR = (Σ u + Σ v)%xnnR.
 
-Axiom xnnreal_sumD :
-  forall u v : xnnreal_seq, (Σ (u + v))%xnnreal = (Σ u + Σ v)%xnnreal.
+Definition isFin (re : xnnR) : Bool :=
+  match re with Fin _ => true | _ => false end.
+
+(* summability is defined in terms of infinite sums *)
+Definition isSummable (u : seq_nnR) := isFin (Σ (Fin o u))%xnnR.
 
 (* the explicit cast functions between both types are a trivial extension and a truncation
    yielding a default value in the case of infinity *)
 
-Definition extend (r : nnreal) : xnnreal := Fin r.
+Definition extend (r : nnR) : xnnR := Fin r.
 
-Definition truncate (re : xnnreal) : nnreal :=
+Definition truncate (re : xnnR) : nnR :=
   match re with
-  | Inf => nnreal_zero
+  | Inf => 0%nnR
   | Fin r => r
   end.
 
-Definition is_finite (re : xnnreal) : Bool :=
-  match re with Inf => false | Fin _ => true end.
-
-Definition cv_sum (u : nnreal_seq) := is_finite
-  (Σ (Fin o u))%xnnreal.
+Record summable :=
+  { to_seq :> seq_nnR; isSummableP : isSummable to_seq = true }.
+Declare Scope summable_scope.
+Delimit Scope summable_scope with summable.
+Bind Scope summable_scope with summable.
 
-(* TODO: expliquer cet encodage? *)
+Axiom summable_add :
+  forall u v : summable, isSummable (fun n => u n + v n)%nnR = true.
 
-Record nnreal_cv_seq := {
-   cv_to_nnreal_seq :> nnreal_seq;
-   nnreal_cv_seq_finite_sum : cv_sum cv_to_nnreal_seq = true
-}.
-Declare Scope nnreal_cv_seq_scope.
-Delimit Scope nnreal_cv_seq_scope with nnreal_cv_seq.
-Bind Scope nnreal_cv_seq_scope with nnreal_cv_seq.
+Definition add_summable (u v : summable) :=
+  Build_summable _ (summable_add u v).
+Infix "+" := add_summable : summable_scope.
 
-Axiom add_nnreal_seq_cv :
-  forall u v : nnreal_cv_seq, cv_sum (fun n => u n + v n)%nnreal = true.
-
-Definition add_nnreal_cv_seq (u v : nnreal_cv_seq) :=
-  Build_nnreal_cv_seq _ (add_nnreal_seq_cv u v).
-Infix "+" := add_nnreal_cv_seq : nnreal_cv_seq_scope.
-
-Definition nnreal_sum (u : nnreal_cv_seq) : nnreal :=
-  truncate (xnnreal_sum (Fin o u)).
-Notation "'Σ' u" := (nnreal_sum u) (at level 35) : nnreal_scope.
+Definition sum_nnR (u : summable) : nnR :=
+  truncate (sum_xnnR (Fin o u)).
+Notation "'Σ' u" := (sum_nnR u) (at level 35) : nnR_scope.
 
 (* various proofs to be used as fields of the parametricity witness *)
 
-Definition R_nnreal (r : nnreal) (re : xnnreal) : Type := extend r = re.
+Definition R_nnR (r : nnR) (re : xnnR) : Type := extend r = re.
 
-Definition truncate_extend : forall (r : nnreal), truncate (extend r) = r.
+Definition truncate_extend : forall (r : nnR), truncate (extend r) = r.
 Proof. reflexivity. Defined.
 
 (* in this way, the composition is an identity only conditionally *)
-(* this is why truncate_in_R_nnreal is not provable and the maximum provable class is (4,2b) *)
+(* this is why truncate_in_R_nnR is not provable and the maximum provable class is (4,2b) *)
 Definition extend_truncate :
-  forall (re : xnnreal), is_finite re = true -> extend (truncate re) = re.
+  forall (re : xnnR), isFin re = true -> extend (truncate re) = re.
 Proof. by case => //=; discriminate. Defined.
 
-Definition extend_in_R_nnreal (r : nnreal) (re : xnnreal) (e : extend r = re) : R_nnreal r re := e.
-Definition R_in_extend_nnreal (r : nnreal) (re : xnnreal) (w : R_nnreal r re) : extend r = re := w.
-Definition R_in_extendK_nnreal (r : nnreal) (re : xnnreal) (w : R_nnreal r re) :
-  extend_in_R_nnreal r re (R_in_extend_nnreal r re w) = w.
+Definition extend_in_R_nnR (r : nnR) (re : xnnR) (e : extend r = re) : R_nnR r re := e.
+Definition R_in_extend_nnR (r : nnR) (re : xnnR) (w : R_nnR r re) : extend r = re := w.
+Definition R_in_extendK_nnR (r : nnR) (re : xnnR) (w : R_nnR r re) :
+  extend_in_R_nnR r re (R_in_extend_nnR r re w) = w.
 Proof. reflexivity. Defined.
-Definition truncate_in_R_nnreal (r : nnreal) (re : xnnreal) (e : truncate re = r) : R_nnreal r re.
-Proof. rewrite <- e; unfold R_nnreal. apply extend_truncate. Abort.
-Definition R_in_truncate_nnreal (re : xnnreal) (r : nnreal) (w : R_nnreal r re) : truncate re = r.
+Definition truncate_in_R_nnR (r : nnR) (re : xnnR) (e : truncate re = r) : R_nnR r re.
+Proof. rewrite <- e; unfold R_nnR. apply extend_truncate. Abort.
+Definition R_in_truncate_nnR (re : xnnR) (r : nnR) (w : R_nnR r re) : truncate re = r.
 Proof. rewrite <- w. apply truncate_extend. Defined.
 
 (* maximum witness between non negative reals and their extended version *)
-Definition Param42b_nnreal : Param42b.Rel nnreal xnnreal.
+Definition Param42b_nnR : Param42b.Rel nnR xnnR.
 Proof.
   unshelve econstructor.
-  - exact R_nnreal.
+  - exact R_nnR.
   - unshelve econstructor.
     + exact extend.
-    + exact extend_in_R_nnreal.
-    + exact R_in_extend_nnreal.
-    + exact R_in_extendK_nnreal.
+    + exact extend_in_R_nnR.
+    + exact R_in_extend_nnR.
+    + exact R_in_extendK_nnR.
   - unshelve econstructor.
     + exact truncate.
-    + exact R_in_truncate_nnreal.
+    + exact R_in_truncate_nnR.
 Defined.
 
 (* the only level we will need to pre-process the distributivity goal is (0,2b) *)
-Definition Param02b_nnreal : Param02b.Rel nnreal xnnreal := Param42b_nnreal.
+Definition Param02b_nnR : Param02b.Rel nnR xnnR := Param42b_nnR.
 
 (* as sequences are encoded with constants, we need to relate them *)
 
-Definition seq_extend (u : nnreal_cv_seq) : xnnreal_seq :=
+Definition seq_extend (u : summable) : seq_xnnR :=
   fun n => extend (u n).
-Definition Rrseq (u : nnreal_cv_seq) (v : xnnreal_seq) : Type :=
+Definition Rrseq (u : summable) (v : seq_xnnR) : Type :=
   seq_extend u = v.
 Definition extend_in_Rrseq
-  (r : nnreal_cv_seq) (re : xnnreal_seq) (e : seq_extend r = re) : Rrseq r re := e.
+  (r : summable) (re : seq_xnnR) (e : seq_extend r = re) : Rrseq r re := e.
 Definition R_in_extend_rseq
-  (r : nnreal_cv_seq) (re : xnnreal_seq) (w : Rrseq r re) : seq_extend r = re := w.
-Definition R_in_extendK_rseq (r : nnreal_cv_seq) (re : xnnreal_seq) (w : Rrseq r re) :
+  (r : summable) (re : seq_xnnR) (w : Rrseq r re) : seq_extend r = re := w.
+Definition R_in_extendK_rseq (r : summable) (re : seq_xnnR) (w : Rrseq r re) :
   extend_in_Rrseq r re (R_in_extend_rseq r re w) = w.
 Proof. reflexivity. Defined.
 
-(* TODO: est-ce que (4,0) est le max ou on ne s'est simplement pas embêté? *)
-Definition Param40_rseq : Param40.Rel nnreal_cv_seq xnnreal_seq.
+(* we could go up to Param42b, but no further *)
+Definition Param40_rseq : Param40.Rel summable seq_xnnR.
 Proof.
   unshelve econstructor.
   - exact Rrseq.
@@ -178,69 +175,44 @@ Definition Param2a0_rseq : Param2a0.Rel _ _ := Param40_rseq.
 
 (* now we need to relate the various constants at level (0,0) *)
 
-Definition R_xnnreal_add :
-  forall (r1 : nnreal) (re1 : xnnreal), R_nnreal r1 re1 ->
-  forall (r2 : nnreal) (re2 : xnnreal), R_nnreal r2 re2 ->
-    R_nnreal (r1 + r2) (re1 + re2).
+Definition R_add_xnnR :
+  forall (r1 : nnR) (re1 : xnnR), R_nnR r1 re1 ->
+  forall (r2 : nnR) (re2 : xnnR), R_nnR r2 re2 ->
+    R_nnR (r1 + r2) (re1 + re2).
 Proof.
-rewrite /R_nnreal /extend.
+rewrite /R_nnR /extend.
 move=> r1 [_ []|]; last by discriminate.
 by move=> r2 [_ []|]; last by discriminate.
 Qed.
 
-Definition R_nnreal_seq_add :
-  forall (r1 : nnreal_cv_seq) (re1 : xnnreal_seq), Rrseq r1 re1 ->
-  forall (r2 : nnreal_cv_seq) (re2 : xnnreal_seq), Rrseq r2 re2 ->
+Definition seq_nnR_add :
+  forall (r1 : summable) (re1 : seq_xnnR), Rrseq r1 re1 ->
+  forall (r2 : summable) (re2 : seq_xnnR), Rrseq r2 re2 ->
   Rrseq (r1 + r2) (re1 + re2).
 Proof.
 move=> [r1 r1cv] re1 <-.
 by move=> [r2 r2cv] re2 <-.
 Qed.
 
-Definition R_xnnreal_sum :
-  forall (u : nnreal_cv_seq) (ue : xnnreal_seq),
-     Rrseq u ue -> R_nnreal (Σ u) (Σ ue).
+Definition R_sum_xnnR :
+  forall (u : summable) (ue : seq_xnnR),
+     Rrseq u ue -> R_nnR (Σ u) (Σ ue).
 Proof.
-rewrite /Rrseq /seq_extend /R_nnreal /nnreal_sum.
+rewrite /Rrseq /seq_extend /R_nnR /sum_nnR.
 move=> u _ <-; rewrite extend_truncate//.
-by apply nnreal_cv_seq_finite_sum.
+by apply isSummableP.
 Qed.
 
-Elpi Query param lp:{{
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref
-        {{:gref paths}} (pc map0 map1)
-        [pc map0 map2b]
-        {{:gref paths}} {{:gref Param01_paths}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref nnreal}} (pc map0 map2b) [] {{:gref xnnreal}}
-        {{:gref Param02b_nnreal}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref nnreal_cv_seq}} (pc map2a map0) [] {{:gref xnnreal_seq}}
-        {{:gref Param2a0_rseq}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref nnreal_sum}} (pc map0 map0) [] {{:gref xnnreal_sum}}
-        {{:gref R_xnnreal_sum}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref nnreal_add}} (pc map0 map0) [] {{:gref xnnreal_add}}
-        {{:gref R_xnnreal_add}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref add_nnreal_cv_seq}} (pc map0 map0) [] {{:gref add_xnnreal_seq}}
-        {{:gref R_nnreal_seq_add}})).
-}}.
+Trocq Use Param01_paths.
+Trocq Use Param02b_nnR.
+Trocq Use Param2a0_rseq.
+Trocq Use R_sum_xnnR.
+Trocq Use R_add_xnnR.
+Trocq Use seq_nnR_add.
 
 (* we get a proof over non negative reals for free,
    from the analogous proof over the extended ones *)
-Lemma nnreal_cv_sumD : forall (u v : nnreal_cv_seq), (Σ (u + v) = Σ u + Σ v)%nnreal.
-Proof.
-  param.
-  exact: xnnreal_sumD.
-Qed.
+Lemma sum_nnR_add : forall (u v : summable), (Σ (u + v) = Σ u + Σ v)%nnR.
+Proof. trocq; exact: sum_xnnR_add. Qed.
 
-Print Assumptions nnreal_cv_sumD.
+Print Assumptions sum_nnR_add.
diff --git a/examples/trocq_gen_rewrite.v b/examples/trocq_gen_rewrite.v
index 08d9dca..cec5765 100644
--- a/examples/trocq_gen_rewrite.v
+++ b/examples/trocq_gen_rewrite.v
@@ -1,19 +1,19 @@
-(**************************************************************************************************)
-(*                            *                               Trocq                               *)
-(*  _______                   *                      Copyright (C) 2023 MERCE                     *)
-(* |__   __|                  *               (Mitsubishi Electric R&D Centre Europe)             *)
-(*    | |_ __ ___   ___ __ _  *                  Cyril Cohen <cyril.cohen@inria.fr>               *)
-(*    | | '__/ _ \ / __/ _` | *                  Enzo Crance <enzo.crance@inria.fr>               *)
-(*    | | | | (_) | (_| (_| | *              Assia Mahboubi <assia.mahboubi@inria.fr>             *)
-(*    |_|_|  \___/ \___\__, | *********************************************************************)
-(*                        | | *           This file is distributed under the terms of the         *)
-(*                        |_| *             GNU Lesser General Public License Version 3           *)
-(*                            *            (see LICENSE file for the text of the license)         *)
-(**************************************************************************************************)
+(*****************************************************************************)
+(*                            *                    Trocq                     *)
+(*  _______                   *           Copyright (C) 2023 MERCE           *)
+(* |__   __|                  *    (Mitsubishi Electric R&D Centre Europe)   *)
+(*    | |_ __ ___   ___ __ _  *       Cyril Cohen <cyril.cohen@inria.fr>     *)
+(*    | | '__/ _ \ / __/ _` | *       Enzo Crance <enzo.crance@inria.fr>     *)
+(*    | | | | (_) | (_| (_| | *   Assia Mahboubi <assia.mahboubi@inria.fr>   *)
+(*    |_|_|  \___/ \___\__, | ************************************************)
+(*                        | | * This file is distributed under the terms of  *)
+(*                        |_| * GNU Lesser General Public License Version 3  *)
+(*                            * see LICENSE file for the text of the license *)
+(*****************************************************************************)
 
 From Coq Require Import ssreflect.
 From HoTT Require Import HoTT.
-From Trocq Require Import HoTT_additions Hierarchy Param Param_paths.
+From Trocq Require Import Trocq.
 
 Set Universe PolymoRinthism.
 
@@ -57,32 +57,20 @@ apply: (@Param01.BuildRel (m <= n)%int (m' <= n')%int (fun _ _ => Unit)).
 - by constructor => mn; apply (le_morph _ _ Rm _ _ Rn).
 Qed.
 
-Elpi Query param lp:{{
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref le}} (pc map0 map1) [] {{:gref le}} {{:gref le01}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref add}} (pc map0 map0) [] {{:gref add}} {{:gref add_morph}})).
-}}.
+Trocq Use le01.
+Trocq Use add_morph.
 
 Variables i j : int.
 Variable ip : (j <= i)%int.
 Definition iid : (i <= i)%int := le_refl i.
 
-Elpi Query param lp:{{
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref j}} (pc map0 map0) [] {{:gref i}} {{:gref ip}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref i}} (pc map0 map0) [] {{:gref i}} {{:gref iid}})).
-}}.
+Trocq Use ip.
+Trocq Use iid.
 
 Example ipi : (j + i + j <= i + i + i)%int.
 Proof.
-param.
+trocq.
 apply le_refl.
 Qed.
 Print ipi.
-Print Assumptions ipi.
\ No newline at end of file
+Print Assumptions ipi.
diff --git a/examples/trocq_setoid_rewrite.v b/examples/trocq_setoid_rewrite.v
index 11b5728..fc56e2f 100644
--- a/examples/trocq_setoid_rewrite.v
+++ b/examples/trocq_setoid_rewrite.v
@@ -1,19 +1,19 @@
-(**************************************************************************************************)
-(*                            *                               Trocq                               *)
-(*  _______                   *                      Copyright (C) 2023 MERCE                     *)
-(* |__   __|                  *               (Mitsubishi Electric R&D Centre Europe)             *)
-(*    | |_ __ ___   ___ __ _  *                  Cyril Cohen <cyril.cohen@inria.fr>               *)
-(*    | | '__/ _ \ / __/ _` | *                  Enzo Crance <enzo.crance@inria.fr>               *)
-(*    | | | | (_) | (_| (_| | *              Assia Mahboubi <assia.mahboubi@inria.fr>             *)
-(*    |_|_|  \___/ \___\__, | *********************************************************************)
-(*                        | | *           This file is distributed under the terms of the         *)
-(*                        |_| *             GNU Lesser General Public License Version 3           *)
-(*                            *            (see LICENSE file for the text of the license)         *)
-(**************************************************************************************************)
+(*****************************************************************************)
+(*                            *                    Trocq                     *)
+(*  _______                   *           Copyright (C) 2023 MERCE           *)
+(* |__   __|                  *    (Mitsubishi Electric R&D Centre Europe)   *)
+(*    | |_ __ ___   ___ __ _  *       Cyril Cohen <cyril.cohen@inria.fr>     *)
+(*    | | '__/ _ \ / __/ _` | *       Enzo Crance <enzo.crance@inria.fr>     *)
+(*    | | | | (_) | (_| (_| | *   Assia Mahboubi <assia.mahboubi@inria.fr>   *)
+(*    |_|_|  \___/ \___\__, | ************************************************)
+(*                        | | * This file is distributed under the terms of  *)
+(*                        |_| * GNU Lesser General Public License Version 3  *)
+(*                            * see LICENSE file for the text of the license *)
+(*****************************************************************************)
 
 From Coq Require Import ssreflect.
 From HoTT Require Import HoTT.
-From Trocq Require Import HoTT_additions Hierarchy Param Param_paths.
+From Trocq Require Import Trocq.
 
 Set Universe PolymoRinthism.
 
@@ -55,34 +55,22 @@ apply: (@Param01.BuildRel (m == n)%int (m' == n')%int (fun _ _ => Unit)).
 - by constructor => mn; apply (eqmodp_morph _ _ Rm _ _ Rn).
 Qed.
 
-Elpi Query param lp:{{
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref eqmodp}} (pc map0 map1) [] {{:gref eqmodp}} {{:gref eqmodp01}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref add}} (pc map0 map0) [] {{:gref add}} {{:gref add_morph}})).
-}}.
+Trocq Use eqmodp01.
+Trocq Use add_morph.
 
 Variables i : int.
 Let j := (i + p)%int.
 Variable ip : (j == i)%int.
 Definition iid : (i == i)%int := eqp_refl i.
 
-Elpi Query param lp:{{
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref j}} (pc map0 map0) [] {{:gref i}} {{:gref ip}})),
-  coq.elpi.accumulate _ "param.db"
-    (clause _ (before "default-gref")
-      (param.db.gref {{:gref i}} (pc map0 map0) [] {{:gref i}} {{:gref iid}})).
-}}.
+Trocq Use ip.
+Trocq Use iid.
 
 Example ipi : (j + i == i + i)%int.
 Proof.
-param.
+trocq.
 apply eqp_refl.
 Qed.
 
 Print ipi.
-Print Assumptions ipi.
\ No newline at end of file
+Print Assumptions ipi.
diff --git a/theories/Database.v b/theories/Database.v
index 4e8e002..974424d 100644
--- a/theories/Database.v
+++ b/theories/Database.v
@@ -1,128 +1,65 @@
-(**************************************************************************************************)
-(*                            *                               Trocq                               *)
-(*  _______                   *                      Copyright (C) 2023 MERCE                     *)
-(* |__   __|                  *               (Mitsubishi Electric R&D Centre Europe)             *)
-(*    | |_ __ ___   ___ __ _  *                  Cyril Cohen <cyril.cohen@inria.fr>               *)
-(*    | | '__/ _ \ / __/ _` | *                  Enzo Crance <enzo.crance@inria.fr>               *)
-(*    | | | | (_) | (_| (_| | *              Assia Mahboubi <assia.mahboubi@inria.fr>             *)
-(*    |_|_|  \___/ \___\__, | *********************************************************************)
-(*                        | | *           This file is distributed under the terms of the         *)
-(*                        |_| *             GNU Lesser General Public License Version 3           *)
-(*                            *            (see LICENSE file for the text of the license)         *)
-(**************************************************************************************************)
+(*****************************************************************************)
+(*                            *                    Trocq                     *)
+(*  _______                   *           Copyright (C) 2023 MERCE           *)
+(* |__   __|                  *    (Mitsubishi Electric R&D Centre Europe)   *)
+(*    | |_ __ ___   ___ __ _  *       Cyril Cohen <cyril.cohen@inria.fr>     *)
+(*    | | '__/ _ \ / __/ _` | *       Enzo Crance <enzo.crance@inria.fr>     *)
+(*    | | | | (_) | (_| (_| | *   Assia Mahboubi <assia.mahboubi@inria.fr>   *)
+(*    |_|_|  \___/ \___\__, | ************************************************)
+(*                        | | * This file is distributed under the terms of  *)
+(*                        |_| * GNU Lesser General Public License Version 3  *)
+(*                            * see LICENSE file for the text of the license *)
+(*****************************************************************************)
 
 From Coq Require Import ssreflect.
+From elpi Require Export elpi.
 From HoTT Require Import HoTT.
 Require Import HoTT_additions.
-From elpi Require Import elpi.
-
-(* included to remove Elpi typechecker warnings *)
-From Trocq.Elpi.constraints Extra Dependency "simple-graph.elpi" as simple_graph.
-From Trocq.Elpi.constraints Extra Dependency "constraint-graph.elpi" as constraint_graph.
-From Trocq.Elpi.constraints Extra Dependency "constraints.elpi" as constraints.
-
-From Trocq.Elpi Extra Dependency "annot.elpi" as annot.
-From Trocq.Elpi Extra Dependency "util.elpi" as util.
-From Trocq.Elpi Extra Dependency "param-class.elpi" as param_class.
 
 Set Universe Polymorphism.
 Unset Universe Minimization ToSet.
 
-Elpi Db param.db lp:{{
-  pred param.db.r o:param-class, o:constant.
+Elpi Db trocq.db lp:{{
+  pred trocq.db.r o:param-class, o:constant.
   :name "default-r"
-  param.db.r C R :- var C, !,
-    declare_constraint (param.db.r C R) [C].
-  pred param.db.ptype o:constant.
-  pred param.db.weaken o:constant.
-  pred param.db.param-type o:param-class, o:param-class, o:constant.
-  pred param.db.pparam-type o:param-class, o:constant.
-  param.db.pparam-type C _ :- coq.say "pparam" C, fail.
+  trocq.db.r C R :- var C, !,
+    declare_constraint (trocq.db.r C R) [C].
+
+  pred trocq.db.gref->class o:gref, o:param-class.
+
+  pred trocq.db.ptype o:constant.
+
+  pred trocq.db.weaken o:constant.
+
+  pred trocq.db.param-type o:param-class, o:param-class, o:constant.
+
+  pred trocq.db.pparam-type o:param-class, o:constant.
+  trocq.db.pparam-type C _ :- coq.say "pparam" C, fail.
   :name "default-pparam-type"
-  param.db.pparam-type C PParamType :- var C, !,
-    declare_constraint (param.db.pparam-type C PParamType) [C].
-  pred param.db.param-arrow o:param-class, o:constant.
-  param.db.param-arrow C _ :- coq.say "arrow" C, fail.
+  trocq.db.pparam-type C PParamType :- var C, !,
+    declare_constraint (trocq.db.pparam-type C PParamType) [C].
+
+  pred trocq.db.param-arrow o:param-class, o:constant.
+  trocq.db.param-arrow C _ :- coq.say "arrow" C, fail.
   :name "default-param-arrow"
-  param.db.param-arrow C ParamArrow :- var C, !,
-    declare_constraint (param.db.param-arrow C ParamArrow) [C].
-  pred param.db.param-forall o:param-class, o:constant.
-  param.db.param-forall C _ :- coq.say "forall" C, fail.
+  trocq.db.param-arrow C ParamArrow :- var C, !,
+    declare_constraint (trocq.db.param-arrow C ParamArrow) [C].
+
+  pred trocq.db.param-forall o:param-class, o:constant.
+  trocq.db.param-forall C _ :- coq.say "forall" C, fail.
   :name "default-param-forall"
-  param.db.param-forall C ParamForall :- var C, !,
-    declare_constraint (param.db.param-forall C ParamForall) [C].
-  pred param.db.univalence o:constant.
-  :name "default-univalence"
-  param.db.univalence _ :- coq.error "univalence axiom required".
-  pred param.db.funext o:constant.
-  :name "default-funext"
-  param.db.funext _ :- coq.error "function extensionality axiom required".
-  pred param.db.gref o:gref, o:param-class, o:list param-class, o:gref, o:gref.
-  :name "default-gref"
-  param.db.gref GR Out _ _ _ :- coq.error "cannot find" GR "at out class" Out.
-}}.
+  trocq.db.param-forall C ParamForall :- var C, !,
+    declare_constraint (trocq.db.param-forall C ParamForall) [C].
 
-Elpi Command Param.
-Elpi Accumulate Db param.db.
-Elpi Accumulate File util.
-Elpi Accumulate File annot.
-Elpi Accumulate File param_class.
-Elpi Accumulate File simple_graph.
-Elpi Accumulate File constraint_graph.
-Elpi Accumulate File constraints.
-Elpi Typecheck.
-Elpi Accumulate lp:{{
-  main [str "Register", str "Univalence", str S] :- !, std.do! [
-    std.assert! (coq.locate S GR) "unknown global reference",
-    coq.univ-instance UI0 [],
-    @uinstance! UI0 => coq.env.global GR U,
-    coq.locate "Univalence" GRU,
-    @uinstance! UI0 => coq.env.global GRU ExpectedUTy,
-    coq.typecheck U UTy ok,
-    std.assert-ok! (coq.unify-eq UTy ExpectedUTy) {std.string.concat "" [
-      "type mismatch, expected ",
-      {coq.term->string ExpectedUTy},
-      ", got ",
-      {coq.term->string UTy},
-      "."
-    ]},
-    GR = const Const,
-    coq.elpi.accumulate _ "param.db"
-      (clause _ (before "default-univalence") (param.db.univalence Const)),
-    coq.say "Univalence axiom successfully registered."
-  ].
-  
-  main [str "Register", str "Funext", str S] :- !, std.do! [
-    std.assert! (coq.locate S GR) "unknown global reference",
-    coq.univ-instance UI0 [],
-    @uinstance! UI0 => coq.env.global GR F,
-    coq.locate "Funext" GRF,
-    @uinstance! UI0 => coq.env.global GRF ExpectedFTy,
-    coq.typecheck F FTy ok,
-    std.assert-ok! (coq.unify-eq FTy ExpectedFTy) {std.string.concat "" [
-      "type mismatch, expected ",
-      {coq.term->string ExpectedFTy},
-      ", got ",
-      {coq.term->string FTy},
-      "."
-    ]},
-    GR = const Const,
-    coq.elpi.accumulate _ "param.db"
-      (clause _ (before "default-funext") (param.db.funext Const)),
-    coq.say "Function extensionality axiom successfully registered."
-  ].
+  pred trocq.db.univalence o:constant.
+  :name "default-univalence"
+  trocq.db.univalence _ :- coq.error "univalence axiom required".
 
-  main [str "Usage"] :- !, coq.say {usage-msg}.
-  main _ :- coq.error {std.string.concat "\n" ["command syntax error", {usage-msg}]}.
+  pred trocq.db.funext o:constant.
+  :name "default-funext"
+  trocq.db.funext _ :- coq.error "function extensionality axiom required".
 
-  pred usage-msg o:string.
-  usage-msg U :-
-    std.string.concat "\n" [
-      "usage:",
-      "- Param Register Univalence <u>",
-      "- Param Register Funext <f>",
-      "", "",
-    ] U.
+  pred trocq.db.gref o:gref, o:param-class, o:list param-class, o:gref, o:gref.
+  :name "default-gref"
+  trocq.db.gref GR Out _ _ _ :- coq.error "cannot find" GR "at out class" Out.
 }}.
-Elpi Typecheck.
-Elpi Export Param.
diff --git a/theories/Hierarchy.v b/theories/Hierarchy.v
index 45158c5..accc31c 100644
--- a/theories/Hierarchy.v
+++ b/theories/Hierarchy.v
@@ -1,15 +1,15 @@
-(**************************************************************************************************)
-(*                            *                               Trocq                               *)
-(*  _______                   *                      Copyright (C) 2023 MERCE                     *)
-(* |__   __|                  *               (Mitsubishi Electric R&D Centre Europe)             *)
-(*    | |_ __ ___   ___ __ _  *                  Cyril Cohen <cyril.cohen@inria.fr>               *)
-(*    | | '__/ _ \ / __/ _` | *                  Enzo Crance <enzo.crance@inria.fr>               *)
-(*    | | | | (_) | (_| (_| | *              Assia Mahboubi <assia.mahboubi@inria.fr>             *)
-(*    |_|_|  \___/ \___\__, | *********************************************************************)
-(*                        | | *           This file is distributed under the terms of the         *)
-(*                        |_| *             GNU Lesser General Public License Version 3           *)
-(*                            *            (see LICENSE file for the text of the license)         *)
-(**************************************************************************************************)
+(*****************************************************************************)
+(*                            *                    Trocq                     *)
+(*  _______                   *           Copyright (C) 2023 MERCE           *)
+(* |__   __|                  *    (Mitsubishi Electric R&D Centre Europe)   *)
+(*    | |_ __ ___   ___ __ _  *       Cyril Cohen <cyril.cohen@inria.fr>     *)
+(*    | | '__/ _ \ / __/ _` | *       Enzo Crance <enzo.crance@inria.fr>     *)
+(*    | | | | (_) | (_| (_| | *   Assia Mahboubi <assia.mahboubi@inria.fr>   *)
+(*    |_|_|  \___/ \___\__, | ************************************************)
+(*                        | | * This file is distributed under the terms of  *)
+(*                        |_| * GNU Lesser General Public License Version 3  *)
+(*                            * see LICENSE file for the text of the license *)
+(*****************************************************************************)
 
 From Coq Require Import ssreflect.
 From HoTT Require Import HoTT.
@@ -75,7 +75,7 @@ End Map4.
 (********************)
 
 Elpi Command genhierarchy.
-Elpi Accumulate Db param.db.
+Elpi Accumulate Db trocq.db.
 Elpi Accumulate File param_class.
 Elpi Accumulate lp:{{
   % generate a module with a record type containing:
@@ -103,12 +103,15 @@ Elpi Accumulate lp:{{
             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 _,
+    @primitive! => @udecl! [L] ff [] ff => coq.env.add-indt RelDecl TrocqInd,
     coq.locate "Rel" Rel,
     coq.locate "R" R,
     % add R to database for later use
     R = const CR,
-    coq.elpi.accumulate _ "param.db" (clause _ (after "default-r") (param.db.r Class 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)),
     % generate projections on the covariant subrecord
     map-class->fields M MFields,
     coq.locate "covariant" Covariant,
diff --git a/theories/HoTT_additions.v b/theories/HoTT_additions.v
index 8d2c8c0..c586e76 100644
--- a/theories/HoTT_additions.v
+++ b/theories/HoTT_additions.v
@@ -1,18 +1,18 @@
-(**************************************************************************************************)
-(*                            *                               Trocq                               *)
-(*  _______                   *                      Copyright (C) 2023 MERCE                     *)
-(* |__   __|                  *               (Mitsubishi Electric R&D Centre Europe)             *)
-(*    | |_ __ ___   ___ __ _  *                  Cyril Cohen <cyril.cohen@inria.fr>               *)
-(*    | | '__/ _ \ / __/ _` | *                  Enzo Crance <enzo.crance@inria.fr>               *)
-(*    | | | | (_) | (_| (_| | *              Assia Mahboubi <assia.mahboubi@inria.fr>             *)
-(*    |_|_|  \___/ \___\__, | *********************************************************************)
-(*                        | | *           This file is distributed under the terms of the         *)
-(*                        |_| *             GNU Lesser General Public License Version 3           *)
-(*                            *            (see LICENSE file for the text of the license)         *)
-(**************************************************************************************************)
+(*****************************************************************************)
+(*                            *                    Trocq                     *)
+(*  _______                   *           Copyright (C) 2023 MERCE           *)
+(* |__   __|                  *    (Mitsubishi Electric R&D Centre Europe)   *)
+(*    | |_ __ ___   ___ __ _  *       Cyril Cohen <cyril.cohen@inria.fr>     *)
+(*    | | '__/ _ \ / __/ _` | *       Enzo Crance <enzo.crance@inria.fr>     *)
+(*    | | | | (_) | (_| (_| | *   Assia Mahboubi <assia.mahboubi@inria.fr>   *)
+(*    |_|_|  \___/ \___\__, | ************************************************)
+(*                        | | * This file is distributed under the terms of  *)
+(*                        |_| * GNU Lesser General Public License Version 3  *)
+(*                            * see LICENSE file for the text of the license *)
+(*****************************************************************************)
 
 From Coq Require Import ssreflect.
-From HoTT Require Import HoTT.
+From HoTT Require Export HoTT.
 
 Set Universe Polymorphism.
 Unset Universe Minimization ToSet.
diff --git a/theories/Param.v b/theories/Param.v
index 6ef2b3a..9585287 100644
--- a/theories/Param.v
+++ b/theories/Param.v
@@ -1,21 +1,21 @@
-(**************************************************************************************************)
-(*                            *                               Trocq                               *)
-(*  _______                   *                      Copyright (C) 2023 MERCE                     *)
-(* |__   __|                  *               (Mitsubishi Electric R&D Centre Europe)             *)
-(*    | |_ __ ___   ___ __ _  *                  Cyril Cohen <cyril.cohen@inria.fr>               *)
-(*    | | '__/ _ \ / __/ _` | *                  Enzo Crance <enzo.crance@inria.fr>               *)
-(*    | | | | (_) | (_| (_| | *              Assia Mahboubi <assia.mahboubi@inria.fr>             *)
-(*    |_|_|  \___/ \___\__, | *********************************************************************)
-(*                        | | *           This file is distributed under the terms of the         *)
-(*                        |_| *             GNU Lesser General Public License Version 3           *)
-(*                            *            (see LICENSE file for the text of the license)         *)
-(**************************************************************************************************)
+(*****************************************************************************)
+(*                            *                    Trocq                     *)
+(*  _______                   *           Copyright (C) 2023 MERCE           *)
+(* |__   __|                  *    (Mitsubishi Electric R&D Centre Europe)   *)
+(*    | |_ __ ___   ___ __ _  *       Cyril Cohen <cyril.cohen@inria.fr>     *)
+(*    | | '__/ _ \ / __/ _` | *       Enzo Crance <enzo.crance@inria.fr>     *)
+(*    | | | | (_) | (_| (_| | *   Assia Mahboubi <assia.mahboubi@inria.fr>   *)
+(*    |_|_|  \___/ \___\__, | ************************************************)
+(*                        | | * This file is distributed under the terms of  *)
+(*                        |_| * GNU Lesser General Public License Version 3  *)
+(*                            * see LICENSE file for the text of the license *)
+(*****************************************************************************)
 
 From elpi Require Import elpi.
 From Coq Require Import ssreflect.
 From HoTT Require Import HoTT.
-Require Import HoTT_additions Hierarchy.
 Require Export Database.
+Require Import HoTT_additions Hierarchy.
 Require Export Param_Type Param_arrow Param_forall.
 
 From Trocq.Elpi Extra Dependency "annot.elpi" as annot.
@@ -35,16 +35,16 @@ Inductive map_class : Set := map0 | map1 | map2a | map2b | map3 | map4.
 
 Elpi Command genpparam.
 Elpi Accumulate File param_class.
-Elpi Accumulate Db param.db.
+Elpi Accumulate Db trocq.db.
 
 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 _ "param.db" (clause _ _ (param.db.ptype PType)),
+  coq.elpi.accumulate _ "trocq.db" (clause _ _ (trocq.db.ptype PType)),
   coq.locate "weaken" (const Weaken),
-  coq.elpi.accumulate _ "param.db" (clause _ _ (param.db.weaken Weaken)).
+  coq.elpi.accumulate _ "trocq.db" (clause _ _ (trocq.db.weaken Weaken)).
 }}.
 
 (* generate
@@ -54,7 +54,7 @@ Elpi Query lp:{{
 
 Elpi Command genpparamtype.
 Elpi Accumulate File param_class.
-Elpi Accumulate Db param.db.
+Elpi Accumulate Db trocq.db.
 Elpi Accumulate lp:{{
   pred generate-branch i:univ-instance, i:param-class, i:param-class, o:term.
   generate-branch UI2 Class RClass (pglobal ParamType UI2) :-
@@ -94,7 +94,7 @@ Elpi Accumulate lp:{{
     PParamType is "PParam" ^ {param-class->string Class} ^ "_Type",
     @udecl! [L, L1] ff [lt L L1] ff =>
       coq.env.add-const PParamType Decl _ @transparent! Const,
-    coq.elpi.accumulate _ "param.db" (clause _ _ (param.db.pparam-type Class Const)).
+    coq.elpi.accumulate _ "trocq.db" (clause _ _ (trocq.db.pparam-type Class Const)).
   
   pred generate-pparam-type44
     i:univ.variable, i:univ.variable, i:param-class.
@@ -107,7 +107,7 @@ Elpi Accumulate lp:{{
     PParamType is "PParam" ^ {param-class->string Class} ^ "_Type",
     @udecl! [L, L1] ff [lt L L1] ff =>
       coq.env.add-const PParamType Decl _ @transparent! Const,
-    coq.elpi.accumulate _ "param.db" (clause _ _ (param.db.pparam-type Class Const)).
+    coq.elpi.accumulate _ "trocq.db" (clause _ _ (trocq.db.pparam-type Class Const)).
 }}.
 Elpi Typecheck.
 
@@ -139,7 +139,7 @@ Elpi Query lp:{{
 }}.
 
 Elpi Tactic param.
-Elpi Accumulate Db param.db.
+Elpi Accumulate Db trocq.db.
 Elpi Accumulate File annot.
 Elpi Accumulate File util.
 Elpi Accumulate File param_class.
@@ -171,7 +171,7 @@ Elpi Accumulate lp:{{
   pred translate-goal i:term, i:param-class, o:term, o:term.
   translate-goal G (pc M N) G' GR' :- std.do! [
     cstr.init,
-    T = (app [pglobal (const {param.db.ptype}) _, {map-class->term M}, {map-class->term N}]),
+    T = (app [pglobal (const {trocq.db.ptype}) _, {map-class->term M}, {map-class->term N}]),
     term->annot-term G AG,
     util.when-debug dbg.steps (
       coq.say "will translate" AG "at level" T,
@@ -199,3 +199,4 @@ Elpi Accumulate lp:{{
 Elpi Typecheck.
 
 Tactic Notation "param" := elpi param.
+Tactic Notation "trocq" := elpi param.
diff --git a/theories/Param44.v b/theories/Param44.v
index db9ce67..da30fc8 100644
--- a/theories/Param44.v
+++ b/theories/Param44.v
@@ -1,15 +1,15 @@
-(**************************************************************************************************)
-(*                            *                               Trocq                               *)
-(*  _______                   *                      Copyright (C) 2023 MERCE                     *)
-(* |__   __|                  *               (Mitsubishi Electric R&D Centre Europe)             *)
-(*    | |_ __ ___   ___ __ _  *                  Cyril Cohen <cyril.cohen@inria.fr>               *)
-(*    | | '__/ _ \ / __/ _` | *                  Enzo Crance <enzo.crance@inria.fr>               *)
-(*    | | | | (_) | (_| (_| | *              Assia Mahboubi <assia.mahboubi@inria.fr>             *)
-(*    |_|_|  \___/ \___\__, | *********************************************************************)
-(*                        | | *           This file is distributed under the terms of the         *)
-(*                        |_| *             GNU Lesser General Public License Version 3           *)
-(*                            *            (see LICENSE file for the text of the license)         *)
-(**************************************************************************************************)
+(*****************************************************************************)
+(*                            *                    Trocq                     *)
+(*  _______                   *           Copyright (C) 2023 MERCE           *)
+(* |__   __|                  *    (Mitsubishi Electric R&D Centre Europe)   *)
+(*    | |_ __ ___   ___ __ _  *       Cyril Cohen <cyril.cohen@inria.fr>     *)
+(*    | | '__/ _ \ / __/ _` | *       Enzo Crance <enzo.crance@inria.fr>     *)
+(*    | | | | (_) | (_| (_| | *   Assia Mahboubi <assia.mahboubi@inria.fr>   *)
+(*    |_|_|  \___/ \___\__, | ************************************************)
+(*                        | | * This file is distributed under the terms of  *)
+(*                        |_| * GNU Lesser General Public License Version 3  *)
+(*                            * see LICENSE file for the text of the license *)
+(*****************************************************************************)
 
 From elpi Require Import elpi.
 From Coq Require Import ssreflect.
diff --git a/theories/Param_Type.v b/theories/Param_Type.v
index 465ccdd..104eaff 100644
--- a/theories/Param_Type.v
+++ b/theories/Param_Type.v
@@ -1,15 +1,15 @@
-(**************************************************************************************************)
-(*                            *                               Trocq                               *)
-(*  _______                   *                      Copyright (C) 2023 MERCE                     *)
-(* |__   __|                  *               (Mitsubishi Electric R&D Centre Europe)             *)
-(*    | |_ __ ___   ___ __ _  *                  Cyril Cohen <cyril.cohen@inria.fr>               *)
-(*    | | '__/ _ \ / __/ _` | *                  Enzo Crance <enzo.crance@inria.fr>               *)
-(*    | | | | (_) | (_| (_| | *              Assia Mahboubi <assia.mahboubi@inria.fr>             *)
-(*    |_|_|  \___/ \___\__, | *********************************************************************)
-(*                        | | *           This file is distributed under the terms of the         *)
-(*                        |_| *             GNU Lesser General Public License Version 3           *)
-(*                            *            (see LICENSE file for the text of the license)         *)
-(**************************************************************************************************)
+(*****************************************************************************)
+(*                            *                    Trocq                     *)
+(*  _______                   *           Copyright (C) 2023 MERCE           *)
+(* |__   __|                  *    (Mitsubishi Electric R&D Centre Europe)   *)
+(*    | |_ __ ___   ___ __ _  *       Cyril Cohen <cyril.cohen@inria.fr>     *)
+(*    | | '__/ _ \ / __/ _` | *       Enzo Crance <enzo.crance@inria.fr>     *)
+(*    | | | | (_) | (_| (_| | *   Assia Mahboubi <assia.mahboubi@inria.fr>   *)
+(*    |_|_|  \___/ \___\__, | ************************************************)
+(*                        | | * This file is distributed under the terms of  *)
+(*                        |_| * GNU Lesser General Public License Version 3  *)
+(*                            * see LICENSE file for the text of the license *)
+(*****************************************************************************)
 
 From elpi Require Import elpi.
 From Coq Require Import ssreflect.
@@ -166,7 +166,7 @@ Defined.
   (for M or N in [2b, 3, 4] PQ is always 44) *)
 
 Elpi Command genparamtype.
-Elpi Accumulate Db param.db.
+Elpi Accumulate Db trocq.db.
 Elpi Accumulate File param_class.
 Elpi Accumulate lp:{{
   pred generate-param-type
@@ -218,7 +218,7 @@ Elpi Accumulate lp:{{
     coq.typecheck Decl _ ok,
     @udecl! [L, L1] ff [lt L L1] ff =>
       coq.env.add-const ParamType Decl _ @transparent! Const,
-    coq.elpi.accumulate _ "param.db" (clause _ _ (param.db.param-type Class RClass Const)).
+    coq.elpi.accumulate _ "trocq.db" (clause _ _ (trocq.db.param-type Class RClass Const)).
 }}.
 Elpi Typecheck.
 
diff --git a/theories/Param_arrow.v b/theories/Param_arrow.v
index 620ab44..c52a334 100644
--- a/theories/Param_arrow.v
+++ b/theories/Param_arrow.v
@@ -1,15 +1,15 @@
-(**************************************************************************************************)
-(*                            *                               Trocq                               *)
-(*  _______                   *                      Copyright (C) 2023 MERCE                     *)
-(* |__   __|                  *               (Mitsubishi Electric R&D Centre Europe)             *)
-(*    | |_ __ ___   ___ __ _  *                  Cyril Cohen <cyril.cohen@inria.fr>               *)
-(*    | | '__/ _ \ / __/ _` | *                  Enzo Crance <enzo.crance@inria.fr>               *)
-(*    | | | | (_) | (_| (_| | *              Assia Mahboubi <assia.mahboubi@inria.fr>             *)
-(*    |_|_|  \___/ \___\__, | *********************************************************************)
-(*                        | | *           This file is distributed under the terms of the         *)
-(*                        |_| *             GNU Lesser General Public License Version 3           *)
-(*                            *            (see LICENSE file for the text of the license)         *)
-(**************************************************************************************************)
+(*****************************************************************************)
+(*                            *                    Trocq                     *)
+(*  _______                   *           Copyright (C) 2023 MERCE           *)
+(* |__   __|                  *    (Mitsubishi Electric R&D Centre Europe)   *)
+(*    | |_ __ ___   ___ __ _  *       Cyril Cohen <cyril.cohen@inria.fr>     *)
+(*    | | '__/ _ \ / __/ _` | *       Enzo Crance <enzo.crance@inria.fr>     *)
+(*    | | | | (_) | (_| (_| | *   Assia Mahboubi <assia.mahboubi@inria.fr>   *)
+(*    |_|_|  \___/ \___\__, | ************************************************)
+(*                        | | * This file is distributed under the terms of  *)
+(*                        |_| * GNU Lesser General Public License Version 3  *)
+(*                            * see LICENSE file for the text of the license *)
+(*****************************************************************************)
 
 From elpi Require Import elpi.
 From Coq Require Import ssreflect.
@@ -23,7 +23,7 @@ Unset Universe Minimization ToSet.
 Local Open Scope param_scope.
 
 Elpi Command genparamarrow.
-Elpi Accumulate Db param.db.
+Elpi Accumulate Db trocq.db.
 Elpi Accumulate File param_class.
 
 (* relation for arrow *)
@@ -250,8 +250,8 @@ Elpi Accumulate lp:{{
     coq.typecheck Decl _ ok,
     @udecl! [Li, Lj, Lk] ff [le Li Lk, le Lj Lk] ff =>
       coq.env.add-const ParamArrow Decl _ @transparent! Const,
-    coq.elpi.accumulate _ "param.db" (clause _ (after "default-param-arrow")
-      (param.db.param-arrow Class Const)).
+    coq.elpi.accumulate _ "trocq.db" (clause _ (after "default-param-arrow")
+      (trocq.db.param-arrow Class Const)).
 }}.
 Elpi Typecheck.
 
diff --git a/theories/Param_forall.v b/theories/Param_forall.v
index c7092bf..5c82ab8 100644
--- a/theories/Param_forall.v
+++ b/theories/Param_forall.v
@@ -1,15 +1,15 @@
-(**************************************************************************************************)
-(*                            *                               Trocq                               *)
-(*  _______                   *                      Copyright (C) 2023 MERCE                     *)
-(* |__   __|                  *               (Mitsubishi Electric R&D Centre Europe)             *)
-(*    | |_ __ ___   ___ __ _  *                  Cyril Cohen <cyril.cohen@inria.fr>               *)
-(*    | | '__/ _ \ / __/ _` | *                  Enzo Crance <enzo.crance@inria.fr>               *)
-(*    | | | | (_) | (_| (_| | *              Assia Mahboubi <assia.mahboubi@inria.fr>             *)
-(*    |_|_|  \___/ \___\__, | *********************************************************************)
-(*                        | | *           This file is distributed under the terms of the         *)
-(*                        |_| *             GNU Lesser General Public License Version 3           *)
-(*                            *            (see LICENSE file for the text of the license)         *)
-(**************************************************************************************************)
+(*****************************************************************************)
+(*                            *                    Trocq                     *)
+(*  _______                   *           Copyright (C) 2023 MERCE           *)
+(* |__   __|                  *    (Mitsubishi Electric R&D Centre Europe)   *)
+(*    | |_ __ ___   ___ __ _  *       Cyril Cohen <cyril.cohen@inria.fr>     *)
+(*    | | '__/ _ \ / __/ _` | *       Enzo Crance <enzo.crance@inria.fr>     *)
+(*    | | | | (_) | (_| (_| | *   Assia Mahboubi <assia.mahboubi@inria.fr>   *)
+(*    |_|_|  \___/ \___\__, | ************************************************)
+(*                        | | * This file is distributed under the terms of  *)
+(*                        |_| * GNU Lesser General Public License Version 3  *)
+(*                            * see LICENSE file for the text of the license *)
+(*****************************************************************************)
 
 From elpi Require Import elpi.
 From Coq Require Import ssreflect.
@@ -23,7 +23,7 @@ Unset Universe Minimization ToSet.
 Local Open Scope param_scope.
 
 Elpi Command genparamforall.
-Elpi Accumulate Db param.db.
+Elpi Accumulate Db trocq.db.
 Elpi Accumulate File param_class.
 
 (* relation for forall *)
@@ -311,8 +311,8 @@ Elpi Accumulate lp:{{
     coq.typecheck Decl _ ok,
     @udecl! [Li, Lj, Lk] ff [le Li Lk, le Lj Lk] ff =>
       coq.env.add-const ParamForall Decl _ @transparent! Const,
-    coq.elpi.accumulate _ "param.db" (clause _ (after "default-param-forall")
-      (param.db.param-forall Class Const)).
+    coq.elpi.accumulate _ "trocq.db" (clause _ (after "default-param-forall")
+      (trocq.db.param-forall Class Const)).
 }}.
 Elpi Typecheck.
 
diff --git a/theories/Param_option.v b/theories/Param_option.v
index 41d2628..ec39169 100644
--- a/theories/Param_option.v
+++ b/theories/Param_option.v
@@ -1,15 +1,15 @@
-(**************************************************************************************************)
-(*                            *                               Trocq                               *)
-(*  _______                   *                      Copyright (C) 2023 MERCE                     *)
-(* |__   __|                  *               (Mitsubishi Electric R&D Centre Europe)             *)
-(*    | |_ __ ___   ___ __ _  *                  Cyril Cohen <cyril.cohen@inria.fr>               *)
-(*    | | '__/ _ \ / __/ _` | *                  Enzo Crance <enzo.crance@inria.fr>               *)
-(*    | | | | (_) | (_| (_| | *              Assia Mahboubi <assia.mahboubi@inria.fr>             *)
-(*    |_|_|  \___/ \___\__, | *********************************************************************)
-(*                        | | *           This file is distributed under the terms of the         *)
-(*                        |_| *             GNU Lesser General Public License Version 3           *)
-(*                            *            (see LICENSE file for the text of the license)         *)
-(**************************************************************************************************)
+(*****************************************************************************)
+(*                            *                    Trocq                     *)
+(*  _______                   *           Copyright (C) 2023 MERCE           *)
+(* |__   __|                  *    (Mitsubishi Electric R&D Centre Europe)   *)
+(*    | |_ __ ___   ___ __ _  *       Cyril Cohen <cyril.cohen@inria.fr>     *)
+(*    | | '__/ _ \ / __/ _` | *       Enzo Crance <enzo.crance@inria.fr>     *)
+(*    | | | | (_) | (_| (_| | *   Assia Mahboubi <assia.mahboubi@inria.fr>   *)
+(*    |_|_|  \___/ \___\__, | ************************************************)
+(*                        | | * This file is distributed under the terms of  *)
+(*                        |_| * GNU Lesser General Public License Version 3  *)
+(*                            * see LICENSE file for the text of the license *)
+(*****************************************************************************)
 
 From Coq Require Import ssreflect.
 From HoTT Require Import HoTT.
@@ -18,146 +18,129 @@ Require Import HoTT_additions Hierarchy.
 Set Universe Polymorphism.
 Unset Universe Minimization ToSet.
 
-Inductive option (A : Type) : Type :=
-  | none
-  | some : A -> option A.
 
-Inductive optionR A A' (AR : A -> A' -> Type) : option A -> option A' -> Type :=
-  | noneR : optionR none none
-  | someR a a' (aR : AR a a') : optionR (some a) (some a').
-
-(*  *)
-
-Definition prod_map
-  (A A' : Type) (AR : Param10.Rel A A') (B B' : Type) (BR : Param10.Rel B B') :
-    A * B -> A' * B' :=
-      fun p =>
-        match p with
-        | (a, b) => (map AR a, map BR b)
-        end.
-
-(*  *)
-
-Definition pair_inj1 A B (a1 a2 : A) (b1 b2 : B) :
-  (a1, b1) = (a2, b2) -> a1 = a2 :=
-    fun e => 
-      match e in @paths _ _ (a, b) return _ = a with
-      | @idpath _ _ => @idpath _ a1
+Inductive optionR (A A' : Type) (AR : A -> A' -> Type) :
+  option A -> option A' -> Type :=
+    | someR :
+      forall (a : A) (a' : A'), AR a a' ->
+        optionR A A' AR (Some a) (Some a')
+    | noneR : optionR A A' AR None None.
+
+Definition option_map :
+forall (A A' : Type) (AR : Param10.Rel A A'), option A -> option A' :=
+  fun A A' AR =>
+    fun oa =>
+      match oa in option _ return option A' with
+      | Some a => Some (map AR a)
+      | None => None
       end.
 
-Definition pair_inj2 A B (a1 a2 : A) (b1 b2 : B) :
-  (a1, b1) = (a2, b2) -> b1 = b2 :=
-    fun e => 
-      match e in @paths _ _ (a, b) return _ = b with
-      | @idpath _ _ => @idpath _ b1
-      end.
-
-Definition prod_map_in_R
-  (A A' : Type) (AR : Param2a0.Rel A A') (B B' : Type) (BR : Param2a0.Rel B B') :
-    forall p p', prod_map A A' AR B B' BR p = p' -> prodR A A' AR B B' BR p p' :=
-  fun p p' =>
-    match p with
-    | (a, b) =>
-      match p' with
-      | (a', b') =>
-        fun e =>
-          pairR A A' AR B B' BR
-            a a' (map_in_R AR a a' (pair_inj1 A' B' (map AR a) a' (map BR b) b' e))
-            b b' (map_in_R BR b b' (pair_inj2 A' B' (map AR a) a' (map BR b) b' e))
+Definition some_inj1 :
+forall (A : Type) (a1 a2 : A), Some a1 = Some a2 -> a1 = a2 :=
+  fun A a1 a2 e =>
+    let proj1 (oa : option A) :=
+      match oa with
+      | Some a => a
+      | None => a1
       end
-    end.
+    in ap proj1 e.
+
+Definition exfalso_option_some_none :
+  forall (T : Type) (A : Type) (a : A), Some a = None -> T :=
+    fun T A a e =>
+      match e in @paths _ _ t
+      return
+        match t with
+        | Some _ => Unit
+        | _ => T
+        end
+      with
+      | idpath => tt
+      end.
 
-(*  *)
+Definition exfalso_option_none_some :
+  forall (T : Type) (A : Type) (a : A), None = Some a -> T :=
+    fun T A a e =>
+      match e in @paths _ _ t
+      return
+        match t with
+        | None => Unit
+        | Some _ => T
+        end
+      with
+      | idpath => tt
+      end.
 
-Definition prod_R_in_map
-  (A A' : Type) (AR : Param2b0.Rel A A') (B B' : Type) (BR : Param2b0.Rel B B') :
-    forall p p', prodR A A' AR B B' BR p p' -> prod_map A A' AR B B' BR p = p' :=
-  fun p p' r =>
-    match r with
-    | pairR a a' aR b b' bR =>
-      @transport _ (fun t => (t, map BR b) = (a', b')) _ _ (R_in_map AR a a' aR)^
-        (@transport _ (fun t => (a', t) = (a', b')) _ _ (R_in_map BR b b' bR)^ idpath)
-    end.
+Definition option_map_in_R :
+  forall (A A' : Type) (AR : Param2a0.Rel A A')
+         (oa : option A) (oa' : option A'),
+    option_map A A' AR oa = oa' -> optionR A A' AR oa oa' :=
+  fun A A' AR =>
+    fun oa oa' =>
+      match oa with
+      | Some a =>
+        match oa' with
+        | Some a' =>
+          fun e =>
+            someR A A' AR a a' (map_in_R AR a a' (some_inj1 A' (map AR a) a' e))
+        | none =>
+          fun e =>
+            exfalso_option_some_none (optionR A A' AR (Some a) (None))
+              A' (map AR a) e
+        end
+      | none =>
+        match oa' with
+        | Some a' =>
+          fun e =>
+            exfalso_option_none_some (optionR A A' AR (None) (Some a'))
+              A' a' e
+        | none => fun e => noneR A A' AR
+        end
+      end.
 
-(*  *)
 
-Definition ap2 : forall {A B C : Type} {a a' : A} {b b' : B} (f : A -> B -> C),
-  a = a' -> b = b' -> f a b = f a' b' :=
-    fun A B C a a' b b' f e1 e2 =>
-      match e1 with
-      | idpath =>
-        match e2 with
-        | idpath => idpath
-        end
+Definition option_R_in_map :
+  forall (A A' : Type) (AR : Param2b0.Rel A A')
+         (oa : option A) (oa' : option A'),
+    optionR A A' AR oa oa' -> option_map A A' AR oa = oa'
+    :=
+  fun A A' AR =>
+    fun oa oa' oaR =>
+      match oaR in optionR _ _ _ oa oa' return option_map A A' AR oa = oa' with
+      | @someR _ _ _ a a' aR =>
+        @transport A' (fun t => Some t = Some a')
+          a' (map AR a) (R_in_map AR a a' aR)^
+            idpath
+      | @noneR _ _ _ => idpath
       end.
 
-Definition prod_R_in_mapK
-  (A A' : Type) (AR : Param40.Rel A A') (B B' : Type) (BR : Param40.Rel B B') :
-    forall p p' (r : prodR A A' AR B B' BR p p'),
-      prod_map_in_R A A' AR B B' BR p p' (prod_R_in_map A A' AR B B' BR p p' r) = r.
+Definition option_R_in_mapK :
+  forall (A A' : Type) (AR : Param40.Rel A A')
+         (oa : option A) (oa' : option A') (oaR : optionR A A' AR oa oa'),
+    option_map_in_R A A' AR oa oa' (option_R_in_map A A' AR oa oa' oaR) = oaR.
 Proof.
-  intros p p' r.
-  destruct r.
-  apply (ap2 (fun x y => pairR A A' AR B B' BR a a' x b b' y)).
+  refine (
+    fun A A' AR =>
+      fun oa oa' oaR =>
+        match oaR in optionR _ _ _ oa oa'
+        return
+          option_map_in_R A A' AR oa oa' (option_R_in_map A A' AR oa oa' oaR)
+            = oaR
+        with
+        | @someR _ _ _ a a' aR => _
+        | @noneR _ _ _ => _
+        end
+  ).
   - simpl.
+    apply (ap (fun x => someR A A' AR a a' x)).
     assert (H:
       R_in_map AR a a' aR =
-        (pair_inj1 A' B' (map AR a) a' (map BR b) b'
-          (transport (fun t => (t, map BR b) = (a', b')) (R_in_map AR a a' aR)^
-            (transport (fun t => (a', t) = (a', b')) (R_in_map BR b b' bR)^ 1%path)))
-    ). { elim (R_in_map AR a a' aR). elim (R_in_map BR b b' bR). reflexivity. }
+      some_inj1 A' (map AR a) a'
+        (transport (fun t : A' => Some t = Some a')
+          (R_in_map AR a a' aR)^
+          idpath)
+    ). { elim (R_in_map AR a a' aR). reflexivity. }
     rewrite <- H.
     exact (R_in_mapK AR a a' aR).
-  - simpl.
-    assert (H:
-      R_in_map BR b b' bR =
-        (pair_inj2 A' B' (map AR a) a' (map BR b) b'
-          (transport (fun t => (t, map BR b) = (a', b')) (R_in_map AR a a' aR)^
-            (transport (fun t => (a', t) = (a', b')) (R_in_map BR b b' bR)^ 1%path)))
-    ). { elim (R_in_map AR a a' aR). elim (R_in_map BR b b' bR). reflexivity. }
-    rewrite <- H.
-    exact (R_in_mapK BR b b' bR).
-Defined.
-
-Definition Map0_prod A A' (AR : Param00.Rel A A') B B' (BR : Param00.Rel B B') :
-  Map0.Has (prodR A A' AR B B' BR).
-Proof. constructor. Defined.
-
-Definition Map1_prod A A' (AR : Param10.Rel A A') B B' (BR : Param10.Rel B B') :
-  Map1.Has (prodR A A' AR B B' BR).
-Proof. constructor. exact (prod_map A A' AR B B' BR). Defined.
-
-Definition Map2a_prod A A' (AR : Param2a0.Rel A A') B B' (BR : Param2a0.Rel B B') :
-  Map2a.Has (prodR A A' AR B B' BR).
-Proof.
-  unshelve econstructor.
-  - exact (prod_map A A' AR B B' BR).
-  - exact (prod_map_in_R A A' AR B B' BR).
-Defined.
-
-Definition Map2b_prod A A' (AR : Param2b0.Rel A A') B B' (BR : Param2b0.Rel B B') :
-  Map2b.Has (prodR A A' AR B B' BR).
-Proof.
-  unshelve econstructor.
-  - exact (prod_map A A' AR B B' BR).
-  - exact (prod_R_in_map A A' AR B B' BR).
-Defined.
-
-Definition Map3_prod A A' (AR : Param30.Rel A A') B B' (BR : Param30.Rel B B') :
-  Map3.Has (prodR A A' AR B B' BR).
-Proof.
-  unshelve econstructor.
-  - exact (prod_map A A' AR B B' BR).
-  - exact (prod_map_in_R A A' AR B B' BR).
-  - exact (prod_R_in_map A A' AR B B' BR).
-Defined.
-
-Definition Map4_prod A A' (AR : Param40.Rel A A') B B' (BR : Param40.Rel B B') :
-  Map4.Has (prodR A A' AR B B' BR).
-Proof.
-  unshelve econstructor.
-  - exact (prod_map A A' AR B B' BR).
-  - exact (prod_map_in_R A A' AR B B' BR).
-  - exact (prod_R_in_map A A' AR B B' BR).
-  - exact (prod_R_in_mapK A A' AR B B' BR).
+  - reflexivity.
 Defined.
diff --git a/theories/Param_paths.v b/theories/Param_paths.v
index 387cd1d..c8d01cc 100644
--- a/theories/Param_paths.v
+++ b/theories/Param_paths.v
@@ -1,15 +1,15 @@
-(**************************************************************************************************)
-(*                            *                               Trocq                               *)
-(*  _______                   *                      Copyright (C) 2023 MERCE                     *)
-(* |__   __|                  *               (Mitsubishi Electric R&D Centre Europe)             *)
-(*    | |_ __ ___   ___ __ _  *                  Cyril Cohen <cyril.cohen@inria.fr>               *)
-(*    | | '__/ _ \ / __/ _` | *                  Enzo Crance <enzo.crance@inria.fr>               *)
-(*    | | | | (_) | (_| (_| | *              Assia Mahboubi <assia.mahboubi@inria.fr>             *)
-(*    |_|_|  \___/ \___\__, | *********************************************************************)
-(*                        | | *           This file is distributed under the terms of the         *)
-(*                        |_| *             GNU Lesser General Public License Version 3           *)
-(*                            *            (see LICENSE file for the text of the license)         *)
-(**************************************************************************************************)
+(*****************************************************************************)
+(*                            *                    Trocq                     *)
+(*  _______                   *           Copyright (C) 2023 MERCE           *)
+(* |__   __|                  *    (Mitsubishi Electric R&D Centre Europe)   *)
+(*    | |_ __ ___   ___ __ _  *       Cyril Cohen <cyril.cohen@inria.fr>     *)
+(*    | | '__/ _ \ / __/ _` | *       Enzo Crance <enzo.crance@inria.fr>     *)
+(*    | | | | (_) | (_| (_| | *   Assia Mahboubi <assia.mahboubi@inria.fr>   *)
+(*    |_|_|  \___/ \___\__, | ************************************************)
+(*                        | | * This file is distributed under the terms of  *)
+(*                        |_| * GNU Lesser General Public License Version 3  *)
+(*                            * see LICENSE file for the text of the license *)
+(*****************************************************************************)
 
 From Coq Require Import ssreflect.
 From HoTT Require Import HoTT.
@@ -178,4 +178,4 @@ Proof.
   - constructor.
 Defined.
 
-(* todo generator *)
\ No newline at end of file
+(* todo generator *)
diff --git a/theories/Param_prod.v b/theories/Param_prod.v
index 17f03ac..d089e98 100644
--- a/theories/Param_prod.v
+++ b/theories/Param_prod.v
@@ -1,15 +1,15 @@
-(**************************************************************************************************)
-(*                            *                               Trocq                               *)
-(*  _______                   *                      Copyright (C) 2023 MERCE                     *)
-(* |__   __|                  *               (Mitsubishi Electric R&D Centre Europe)             *)
-(*    | |_ __ ___   ___ __ _  *                  Cyril Cohen <cyril.cohen@inria.fr>               *)
-(*    | | '__/ _ \ / __/ _` | *                  Enzo Crance <enzo.crance@inria.fr>               *)
-(*    | | | | (_) | (_| (_| | *              Assia Mahboubi <assia.mahboubi@inria.fr>             *)
-(*    |_|_|  \___/ \___\__, | *********************************************************************)
-(*                        | | *           This file is distributed under the terms of the         *)
-(*                        |_| *             GNU Lesser General Public License Version 3           *)
-(*                            *            (see LICENSE file for the text of the license)         *)
-(**************************************************************************************************)
+(*****************************************************************************)
+(*                            *                    Trocq                     *)
+(*  _______                   *           Copyright (C) 2023 MERCE           *)
+(* |__   __|                  *    (Mitsubishi Electric R&D Centre Europe)   *)
+(*    | |_ __ ___   ___ __ _  *       Cyril Cohen <cyril.cohen@inria.fr>     *)
+(*    | | '__/ _ \ / __/ _` | *       Enzo Crance <enzo.crance@inria.fr>     *)
+(*    | | | | (_) | (_| (_| | *   Assia Mahboubi <assia.mahboubi@inria.fr>   *)
+(*    |_|_|  \___/ \___\__, | ************************************************)
+(*                        | | * This file is distributed under the terms of  *)
+(*                        |_| * GNU Lesser General Public License Version 3  *)
+(*                            * see LICENSE file for the text of the license *)
+(*****************************************************************************)
 
 From Coq Require Import ssreflect.
 From HoTT Require Import HoTT.
diff --git a/theories/Param_sigma.v b/theories/Param_sigma.v
new file mode 100644
index 0000000..3abd423
--- /dev/null
+++ b/theories/Param_sigma.v
@@ -0,0 +1,67 @@
+(*****************************************************************************)
+(*                            *                    Trocq                     *)
+(*  _______                   *           Copyright (C) 2023 MERCE           *)
+(* |__   __|                  *    (Mitsubishi Electric R&D Centre Europe)   *)
+(*    | |_ __ ___   ___ __ _  *       Cyril Cohen <cyril.cohen@inria.fr>     *)
+(*    | | '__/ _ \ / __/ _` | *       Enzo Crance <enzo.crance@inria.fr>     *)
+(*    | | | | (_) | (_| (_| | *   Assia Mahboubi <assia.mahboubi@inria.fr>   *)
+(*    |_|_|  \___/ \___\__, | ************************************************)
+(*                        | | * This file is distributed under the terms of  *)
+(*                        |_| * GNU Lesser General Public License Version 3  *)
+(*                            * see LICENSE file for the text of the license *)
+(*****************************************************************************)
+
+From Coq Require Import ssreflect.
+From HoTT Require Import HoTT.
+Require Import Hierarchy.
+
+Set Universe Polymorphism.
+Unset Universe Minimization ToSet.
+
+Inductive sigR
+  A A' (AR : A -> A' -> Type)
+  P P' (PR : forall a a', AR a a' -> P a -> P' a' -> Type) :
+    {x : A & P x} -> {x' : A' & P' x'} -> Type :=
+      | existR a a' (aR : AR a a') p p' (pR : PR a a' aR p p') :
+        sigR A A' AR P P' PR (a; p) (a'; p').
+
+Definition sig_map
+  (A A' : Type) (AR : Param2a0.Rel A A')
+  (P : A -> Type) (P' : A' -> Type) (PR : forall a a', AR a a' -> Param10.Rel (P a) (P' a')) :
+    {x : A & P x} -> {x' : A' & P' x'} :=
+      fun s => (map AR s.1; map (PR s.1 (map AR s.1) (map_in_R AR s.1 (map AR s.1) idpath)) s.2).
+
+Definition sig_map_in_R
+  (A A' : Type) (AR : Param2a0.Rel A A')
+  (P : A -> Type) (P' : A' -> Type) (PR : forall a a', AR a a' -> Param2a0.Rel (P a) (P' a')) :
+    forall (s : {x : A & P x}) (s' : {x' : A' & P' x'}),
+      sig_map A A' AR P P' PR s = s' -> sigR A A' AR P P' PR s s'.
+Proof.
+move=> x y; case: _ /; exists (map_in_R _ _ _ 1); exact: map_in_R.
+Defined.
+
+Definition sig_R_in_map
+  (A A' : Type) (AR : Param40.Rel A A')
+  (P : A -> Type) (P' : A' -> Type) (PR : forall a a', AR a a' -> Param2b0.Rel (P a) (P' a')) :
+    forall (s : {x : A & P x}) (s' : {x' : A' & P' x'}),
+      sigR A A' AR P P' PR s s' -> sig_map A A' AR P P' PR s = s'.
+Proof.
+  move=> s s'; elim=> a a' aR p p' pR.
+  elim (R_in_map _ _ _ pR).
+  elim (R_in_mapK _ _ _ aR).
+  by elim (R_in_map AR _ _ aR).
+Defined.
+
+Definition sig_R_in_mapK
+  (A A' : Type) (AR : Param40.Rel A A')
+  (P : A -> Type) (P' : A' -> Type) (PR : forall a a', AR a a' -> Param40.Rel (P a) (P' a')) :
+    forall (s : {x : A & P x}) (s' : {x' : A' & P' x'}),
+      (sig_map_in_R A A' AR P P' PR s s') o (sig_R_in_map A A' AR P P' PR s s') == idmap.
+Proof.
+  move=> s s' [a a' aR p p' pR].
+  rewrite /sig_R_in_map /sig_map_in_R /=.
+  elim: {2}_ / (R_in_mapK (PR a a' aR) p p' pR).
+  elim: (R_in_map (PR a a' aR) p p' pR) => /=.
+  elim (R_in_mapK AR a a' aR) => /=.
+  by elim (R_in_map AR a a' aR).
+Qed.
diff --git a/theories/Trocq.v b/theories/Trocq.v
index ec8e117..86ac72d 100644
--- a/theories/Trocq.v
+++ b/theories/Trocq.v
@@ -1,16 +1,18 @@
-(**************************************************************************************************)
-(*                            *                               Trocq                               *)
-(*  _______                   *                      Copyright (C) 2023 MERCE                     *)
-(* |__   __|                  *               (Mitsubishi Electric R&D Centre Europe)             *)
-(*    | |_ __ ___   ___ __ _  *                  Cyril Cohen <cyril.cohen@inria.fr>               *)
-(*    | | '__/ _ \ / __/ _` | *                  Enzo Crance <enzo.crance@inria.fr>               *)
-(*    | | | | (_) | (_| (_| | *              Assia Mahboubi <assia.mahboubi@inria.fr>             *)
-(*    |_|_|  \___/ \___\__, | *********************************************************************)
-(*                        | | *           This file is distributed under the terms of the         *)
-(*                        |_| *             GNU Lesser General Public License Version 3           *)
-(*                            *            (see LICENSE file for the text of the license)         *)
-(**************************************************************************************************)
+(*****************************************************************************)
+(*                            *                    Trocq                     *)
+(*  _______                   *           Copyright (C) 2023 MERCE           *)
+(* |__   __|                  *    (Mitsubishi Electric R&D Centre Europe)   *)
+(*    | |_ __ ___   ___ __ _  *       Cyril Cohen <cyril.cohen@inria.fr>     *)
+(*    | | '__/ _ \ / __/ _` | *       Enzo Crance <enzo.crance@inria.fr>     *)
+(*    | | | | (_) | (_| (_| | *   Assia Mahboubi <assia.mahboubi@inria.fr>   *)
+(*    |_|_|  \___/ \___\__, | ************************************************)
+(*                        | | * This file is distributed under the terms of  *)
+(*                        |_| * GNU Lesser General Public License Version 3  *)
+(*                            * see LICENSE file for the text of the license *)
+(*****************************************************************************)
 
+From elpi Require Export elpi.
+From HoTT Require Export HoTT.
 From Trocq Require Export
   HoTT_additions Hierarchy Param_Type Param_forall Param_arrow Database Param
-  Param_paths.
+  Param_paths Vernac.
diff --git a/theories/Uparam.v b/theories/Uparam.v
index f6184fd..f3d7131 100644
--- a/theories/Uparam.v
+++ b/theories/Uparam.v
@@ -1,15 +1,15 @@
-(**************************************************************************************************)
-(*                            *                               Trocq                               *)
-(*  _______                   *                      Copyright (C) 2023 MERCE                     *)
-(* |__   __|                  *               (Mitsubishi Electric R&D Centre Europe)             *)
-(*    | |_ __ ___   ___ __ _  *                  Cyril Cohen <cyril.cohen@inria.fr>               *)
-(*    | | '__/ _ \ / __/ _` | *                  Enzo Crance <enzo.crance@inria.fr>               *)
-(*    | | | | (_) | (_| (_| | *              Assia Mahboubi <assia.mahboubi@inria.fr>             *)
-(*    |_|_|  \___/ \___\__, | *********************************************************************)
-(*                        | | *           This file is distributed under the terms of the         *)
-(*                        |_| *             GNU Lesser General Public License Version 3           *)
-(*                            *            (see LICENSE file for the text of the license)         *)
-(**************************************************************************************************)
+(*****************************************************************************)
+(*                            *                    Trocq                     *)
+(*  _______                   *           Copyright (C) 2023 MERCE           *)
+(* |__   __|                  *    (Mitsubishi Electric R&D Centre Europe)   *)
+(*    | |_ __ ___   ___ __ _  *       Cyril Cohen <cyril.cohen@inria.fr>     *)
+(*    | | '__/ _ \ / __/ _` | *       Enzo Crance <enzo.crance@inria.fr>     *)
+(*    | | | | (_) | (_| (_| | *   Assia Mahboubi <assia.mahboubi@inria.fr>   *)
+(*    |_|_|  \___/ \___\__, | ************************************************)
+(*                        | | * This file is distributed under the terms of  *)
+(*                        |_| * GNU Lesser General Public License Version 3  *)
+(*                            * see LICENSE file for the text of the license *)
+(*****************************************************************************)
 
 From Coq Require Import ssreflect.
 From HoTT Require Import HoTT.
diff --git a/theories/Vernac.v b/theories/Vernac.v
new file mode 100644
index 0000000..57a733e
--- /dev/null
+++ b/theories/Vernac.v
@@ -0,0 +1,109 @@
+(*****************************************************************************)
+(*                            *                    Trocq                     *)
+(*  _______                   *           Copyright (C) 2023 MERCE           *)
+(* |__   __|                  *    (Mitsubishi Electric R&D Centre Europe)   *)
+(*    | |_ __ ___   ___ __ _  *       Cyril Cohen <cyril.cohen@inria.fr>     *)
+(*    | | '__/ _ \ / __/ _` | *       Enzo Crance <enzo.crance@inria.fr>     *)
+(*    | | | | (_) | (_| (_| | *   Assia Mahboubi <assia.mahboubi@inria.fr>   *)
+(*    |_|_|  \___/ \___\__, | ************************************************)
+(*                        | | * This file is distributed under the terms of  *)
+(*                        |_| * GNU Lesser General Public License Version 3  *)
+(*                            * see LICENSE file for the text of the license *)
+(*****************************************************************************)
+
+From Coq Require Import ssreflect.
+From elpi Require Import elpi.
+From HoTT Require Import HoTT.
+From Trocq Require Import HoTT_additions Hierarchy Param_Type Param_forall
+  Param_arrow Database Param Param_paths.
+
+ (* included to remove Elpi typechecker warnings *)
+From Trocq.Elpi.constraints Extra Dependency "simple-graph.elpi" as simple_graph.
+From Trocq.Elpi.constraints Extra Dependency "constraint-graph.elpi" as constraint_graph.
+From Trocq.Elpi.constraints Extra Dependency "constraints.elpi" as constraints.
+
+From Trocq.Elpi Extra Dependency "annot.elpi" as annot.
+From Trocq.Elpi Extra Dependency "util.elpi" as util.
+From Trocq.Elpi Extra Dependency "param-class.elpi" as param_class.
+
+Elpi Command Trocq.
+Elpi Accumulate Db trocq.db.
+Elpi Accumulate File util.
+Elpi Accumulate File annot.
+Elpi Accumulate File param_class.
+Elpi Accumulate File simple_graph.
+Elpi Accumulate File constraint_graph.
+Elpi Accumulate File constraints.
+Elpi Typecheck.
+Elpi Accumulate lp:{{
+  main [str "Register", str "Univalence", str S] :- !, std.do! [
+    std.assert! (coq.locate S GR) "unknown global reference",
+    coq.univ-instance UI0 [],
+    @uinstance! UI0 => coq.env.global GR U,
+    coq.locate "Univalence" GRU,
+    @uinstance! UI0 => coq.env.global GRU ExpectedUTy,
+    coq.typecheck U UTy ok,
+    std.assert-ok! (coq.unify-eq UTy ExpectedUTy) {std.string.concat "" [
+      "type mismatch, expected ",
+      {coq.term->string ExpectedUTy},
+      ", got ",
+      {coq.term->string UTy},
+      "."
+    ]},
+    GR = const Const,
+    coq.elpi.accumulate _ "trocq.db"
+      (clause _ (before "default-univalence") (trocq.db.univalence Const)),
+    coq.say "Univalence axiom successfully registered."
+  ].
+
+  main [str "Register", str "Funext", str S] :- !, std.do! [
+    std.assert! (coq.locate S GR) "unknown global reference",
+    coq.univ-instance UI0 [],
+    @uinstance! UI0 => coq.env.global GR F,
+    coq.locate "Funext" GRF,
+    @uinstance! UI0 => coq.env.global GRF ExpectedFTy,
+    coq.typecheck F FTy ok,
+    std.assert-ok! (coq.unify-eq FTy ExpectedFTy) {std.string.concat "" [
+      "type mismatch, expected ",
+      {coq.term->string ExpectedFTy},
+      ", got ",
+      {coq.term->string FTy},
+      "."
+    ]},
+    GR = const Const,
+    coq.elpi.accumulate _ "trocq.db"
+      (clause _ (before "default-funext") (trocq.db.funext Const)),
+    coq.say "Function extensionality axiom successfully registered."
+  ].
+
+  main [str "Use", str X] :- !,
+    coq.locate X GR, main [str "Use", trm (global GR)].
+
+  main [str "Use", trm X] :- !, std.do! [
+    coq.term->gref X GRR,
+    coq.env.typeof GRR XTy,
+    param-class.type->classes XTy Class CList GR GR',
+    coq.say "accumultating" GR "@" Class "(" CList ") ~" GR' ":." GRR,
+    coq.elpi.accumulate _ "trocq.db"
+      (clause _ (before "default-gref")
+        (trocq.db.gref GR Class CList GR' GRR))
+  ].
+  % coq.elpi.accumulate _ "trocq.db"
+  %   (clause _ (before "default-gref")
+  %     (trocq.db.gref GR (pc map4 map2b) [] {{:gref int}} {{:gref Rp42b}})),
+
+  main [str "Usage"] :- !, coq.say {usage-msg}.
+  main _ :- coq.error {std.string.concat "\n" ["command syntax error", {usage-msg}]}.
+
+  pred usage-msg o:string.
+  usage-msg U :-
+    std.string.concat "\n" [
+      "usage:",
+      "- Trocq Register Univalence <u>",
+      "- Trocq Register Funext <f>",
+      "- Trocq Use <RTrocq>",
+      "", "",
+    ] U.
+}}.
+Elpi Typecheck.
+Elpi Export Trocq.