diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 542c27b9d6f6..8d64f231166f 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -40,7 +40,7 @@ variables:
   # The $hash is the first 10 characters of the md5 of the Dockerfile. e.g.
   # echo $(md5sum dev/ci/docker/old_ubuntu_lts/Dockerfile | head -c 10)
   # echo $(md5sum dev/ci/docker/edge_ubuntu/Dockerfile | head -c 10)
-  BASE_CACHEKEY: "old_ubuntu_lts-V2025-11-14-69405188ee"
+  BASE_CACHEKEY: "old_ubuntu_lts-V2026-04-13-df80ac3f8b"
   EDGE_CACHEKEY: "edge_ubuntu-V2026-03-19-ac6c1c9705"
   BASE_IMAGE: "$CI_REGISTRY_IMAGE:$BASE_CACHEKEY"
   EDGE_IMAGE: "$CI_REGISTRY_IMAGE:$EDGE_CACHEKEY"
@@ -591,6 +591,7 @@ validate:base:
     CI_TARGETS: "stdlib"
   needs:
     - build:base
+    - plugin:ci-micromega
     - library:ci-stdlib
   only: *full-ci
 
@@ -610,6 +611,7 @@ validate:edge+flambda:
     CI_TARGETS: "stdlib"
   needs:
     - build:edge+flambda
+    - plugin:ci-micromega+flambda
     - library:ci-stdlib+flambda
   variables:
     OPAM_VARIANT: "+flambda"
@@ -622,18 +624,21 @@ library:ci-argosy:
   extends: .ci-template
   needs:
   - build:base
+  - plugin:ci-micromega
   - library:ci-stdlib
 
 library:ci-autosubst:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
 
 library:ci-bbv:
   extends: .ci-template
   needs:
   - build:base
+  - plugin:ci-micromega
   - library:ci-stdlib
 
 library:ci-bedrock2:
@@ -643,6 +648,7 @@ library:ci-bedrock2:
     SAVE_BUILD_CI: "1" # for bedrock2_examples
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - library:ci-coqutil
   - library:ci-kami
@@ -655,6 +661,7 @@ library:ci-bedrock2_examples:
     NJOBS: "1"
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - library:ci-coqutil
   - library:ci-kami
@@ -667,6 +674,7 @@ library:ci-category_theory:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - plugin:ci-equations
   stage: build-2
@@ -675,6 +683,7 @@ library:ci-color:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - plugin:ci-bignums
   stage: build-2
@@ -683,6 +692,7 @@ library:ci-compcert:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - library:ci-flocq
   - library:ci-menhir
@@ -692,18 +702,21 @@ library:ci-coq_performance_tests:
   extends: .ci-template
   needs:
   - build:base
+  - plugin:ci-micromega
   - library:ci-stdlib
 
 library:ci-coq_tools:
   extends: .ci-template
   needs:
   - build:base
+  - plugin:ci-micromega
   - library:ci-stdlib
 
 library:ci-coqprime:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - plugin:ci-bignums
   stage: build-2
@@ -715,6 +728,7 @@ library:ci-coquelicot:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - plugin:ci-elpi_hb
   - library:ci-mathcomp
@@ -724,12 +738,14 @@ library:ci-coqutil:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
 
 library:ci-cross_crypto:
   extends: .ci-template
   needs:
   - build:base
+  - plugin:ci-micromega
   - library:ci-stdlib
   variables:
     SAVE_BUILD_CI: "1" # for the minimizer (no install target available)
@@ -738,18 +754,21 @@ library:ci-engine_bench:
   extends: .ci-template
   needs:
   - build:base
+  - plugin:ci-micromega
   - library:ci-stdlib
 
 library:ci-ext_lib:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
 
 library:ci-fcsl_pcm:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - plugin:ci-elpi_hb
   - library:ci-mathcomp
@@ -762,6 +781,7 @@ library:ci-fiat_crypto:
     SAVE_BUILD_CI: "1" # for fiat_crypto_ocaml
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - library:ci-coqutil
   - library:ci-kami
@@ -777,6 +797,7 @@ library:ci-fiat_crypto_legacy:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - library:ci-coqprime
   stage: build-3+
@@ -789,6 +810,7 @@ library:ci-fiat_crypto_ocaml:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - library:ci-coqutil
   - library:ci-kami
@@ -806,18 +828,21 @@ library:ci-flocq:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
 
 library:ci-kami:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
 
 library:ci-menhir:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
 
 library:ci-oddorder:
@@ -840,6 +865,7 @@ library:ci-corn:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - plugin:ci-bignums
   - plugin:ci-elpi_hb # CoRN uses elpi only (not HB) - depending on ci-elpi_hb reduces CI package count
@@ -853,6 +879,7 @@ library:ci-iris:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - library:ci-autosubst
   stage: build-2
@@ -861,6 +888,7 @@ library:ci-math_classes:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - plugin:ci-bignums
   stage: build-2
@@ -886,6 +914,7 @@ library:ci-mczify:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - plugin:ci-elpi_hb
   - library:ci-mathcomp
@@ -895,6 +924,7 @@ library:ci-algebra_tactics:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - plugin:ci-elpi_hb
   - library:ci-mathcomp
@@ -938,6 +968,7 @@ library:ci-analysis_stdlib:
   - library:ci-bigenough
   - library:ci-analysis
   - plugin:ci-elpi_hb  # for Hierarchy Builder
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   stage: build-3+
 
@@ -945,18 +976,21 @@ library:ci-neural_net_interp:
   extends: .ci-template
   needs:
   - build:base
+  - plugin:ci-micromega
   - library:ci-stdlib
 
 library:ci-paco:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
 
 library:ci-itree:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - library:ci-ext_lib
   - library:ci-paco
@@ -966,6 +1000,7 @@ library:ci-itree_io:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - library:ci-ext_lib
   - library:ci-paco
@@ -977,6 +1012,7 @@ library:ci-simple_io:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - library:ci-ext_lib
   stage: build-2
@@ -985,15 +1021,22 @@ library:ci-simple_io:
   extends: .ci-template
   needs:
   - build:base
+  - plugin:ci-micromega
   - library:ci-stdlib
 
 library:ci-stdlib:
   extends: .ci-template
+  needs:
+  - build:base
+  - plugin:ci-micromega
   variables:
     SAVE_BUILD_CI: "1" # for test suite
 
 library:ci-stdlib+flambda:
   extends: .ci-template-flambda
+  needs:
+  - build:edge+flambda
+  - plugin:ci-micromega+flambda
   variables:
     CI_TARGETS: "stdlib"
     SAVE_BUILD_CI: "1" # for test suite
@@ -1002,6 +1045,7 @@ library:ci-stdlib_test:
   extends: .ci-template
   needs:
   - build:base
+  - plugin:ci-micromega
   - library:ci-stdlib
   stage: build-2
 
@@ -1009,6 +1053,7 @@ library:ci-stdlib_doc:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   stage: build-2
   variables:
@@ -1018,6 +1063,7 @@ library:ci-tlc:
   extends: .ci-template
   needs:
   - build:base
+  - plugin:ci-micromega
   - library:ci-stdlib
 
 library:ci-unimath:
@@ -1027,6 +1073,7 @@ library:ci-verdi_raft:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
 
 library:ci-vst:
@@ -1035,6 +1082,7 @@ library:ci-vst:
     NJOBS: "1"
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - library:ci-flocq
   - library:ci-menhir
@@ -1046,6 +1094,7 @@ library:ci-deriving:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - plugin:ci-elpi_hb
   - library:ci-mathcomp
@@ -1055,6 +1104,7 @@ library:ci-mathcomp_word:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - plugin:ci-elpi_hb
   - library:ci-mathcomp
@@ -1064,6 +1114,7 @@ library:ci-jasmin:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - plugin:ci-elpi_hb
   - library:ci-mathcomp
@@ -1079,6 +1130,7 @@ library:ci-http:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - plugin:ci-elpi_hb
   - library:ci-mathcomp
@@ -1099,12 +1151,14 @@ plugin:ci-aac_tactics:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
 
 plugin:ci-atbr:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
 
 plugin:ci-autosubst_ocaml:
@@ -1114,6 +1168,7 @@ plugin:ci-itauto:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   allow_failure: true
 
@@ -1121,24 +1176,28 @@ plugin:ci-bignums:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
 
 plugin:ci-coinduction:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
 
 plugin:ci-coq_dpdgraph:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
 
 plugin:ci-coqhammer:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
 
 plugin:ci-elpi_hb:
@@ -1153,6 +1212,7 @@ plugin:ci-elpi_test:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - plugin:ci-elpi_hb
   stage: build-2
@@ -1161,6 +1221,7 @@ plugin:ci-hb_test:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - plugin:ci-elpi_hb
   stage: build-2
@@ -1169,6 +1230,7 @@ plugin:ci-equations:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   variables:
     SAVE_BUILD_CI: "1" # for equations_test
@@ -1177,6 +1239,7 @@ plugin:ci-equations_test:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - plugin:ci-equations
   stage: build-2
@@ -1185,12 +1248,14 @@ plugin:ci-fiat_parsers:
   extends: .ci-template
   needs:
   - build:base
+  - plugin:ci-micromega
   - library:ci-stdlib
 
 plugin:ci-lean_importer:
   extends: .ci-template
   needs:
   - build:base
+  - plugin:ci-micromega
   - library:ci-stdlib
 
 plugin:ci-ltac2_compiler:
@@ -1200,16 +1265,29 @@ plugin:ci-metarocq:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - plugin:ci-equations
   - library:ci-ext_lib
   stage: build-2
   timeout: 1h 30min
 
+plugin:ci-micromega:
+  extends: .ci-template
+  variables:
+    SAVE_BUILD_CI: "1" # for test suite
+
+plugin:ci-micromega+flambda:
+  extends: .ci-template-flambda
+  variables:
+    CI_TARGETS: "micromega"
+    SAVE_BUILD_CI: "1" # for test suite
+
 plugin:ci-mtac2:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   variables:
     CI_TARGETS: "unicoq mtac2"
@@ -1218,12 +1296,14 @@ plugin:ci-paramcoq:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
 
 plugin:ci-perennial:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
 
 plugin:plugin-tutorial:
@@ -1238,6 +1318,7 @@ plugin:ci-quickchick:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - library:ci-ext_lib
   - library:ci-simple_io
@@ -1251,6 +1332,7 @@ plugin:ci-quickchick_test:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - library:ci-ext_lib
   - library:ci-simple_io
@@ -1266,6 +1348,7 @@ plugin:ci-relation_algebra:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - plugin:ci-elpi_hb
   - library:ci-mathcomp
@@ -1276,12 +1359,14 @@ plugin:ci-rewriter:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
 
 library:ci-riscv_coq:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - library:ci-coqutil
   stage: build-2
@@ -1290,6 +1375,7 @@ library:ci-rupicola:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - library:ci-coqutil
   - library:ci-kami
@@ -1303,6 +1389,7 @@ library:ci-rupicola:
 #   extends: .ci-template-flambda
 #   needs:
 #   - build:edge+flambda
+#   - plugin:ci-micromega+flambda
 #   - library:ci-stdlib+flambda
 
 plugin:ci-vsrocq:
@@ -1312,12 +1399,14 @@ plugin:ci-smtcoq:
   extends: .ci-template
   needs:
   - build:base
+  - plugin:ci-micromega
   - library:ci-stdlib
 
 plugin:ci-stalmarck:
   extends: .ci-template
   needs:
   - build:base
+  - plugin:ci-micromega
   - library:ci-stdlib
 
 plugin:ci-tactician:
@@ -1327,12 +1416,14 @@ plugin:ci-waterproof:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
 
 doc:ci-refman:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
+  - plugin:ci-micromega+flambda
   - library:ci-stdlib+flambda
   - plugin:ci-elpi_hb
   - library:ci-mathcomp
diff --git a/Makefile.ci b/Makefile.ci
index 46933008afdf..4dc6e6f67277 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -28,6 +28,7 @@ CI_PLATFORM_FULL= \
     ci-mathcomp \
     ci-mathcomp_word \
     ci-mczify \
+    ci-micromega \
     ci-algebra_tactics \
     ci-finmap \
     ci-bigenough \
@@ -245,6 +246,8 @@ ci-smtcoq_trakt: ci-stdlib ci-trakt
 
 ci-stalmarck: ci-stdlib
 
+ci-stdlib: ci-micromega
+
 ci-stdlib_test: ci-stdlib
 ci-stdlib_doc: ci-stdlib
 
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index a16ddf5de664..82936047b1dc 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -389,6 +389,12 @@ project async_test "https://github.com/liyishuai/coq-async-test" "master"
 project http "https://github.com/liyishuai/coq-http" "master"
 # Contact @liyishuai on github
 
+########################################################################
+# micromega-plugin
+########################################################################
+project micromega "https://github.com/rocq-community/micromega-plugin" "master"
+# Contact @fajb, @proux01 on github
+
 ########################################################################
 # paramcoq
 ########################################################################
diff --git a/dev/ci/docker/old_ubuntu_lts/Dockerfile b/dev/ci/docker/old_ubuntu_lts/Dockerfile
index ee78cfc0a945..9daf9663fb83 100644
--- a/dev/ci/docker/old_ubuntu_lts/Dockerfile
+++ b/dev/ci/docker/old_ubuntu_lts/Dockerfile
@@ -52,7 +52,7 @@ ENV COMPILER="4.14.0"
 # Common OPAM packages
 ENV BASE_OPAM="zarith.1.11 ounit2.2.2.6 yojson.1.7.0 camlzip.1.10" \
     CI_OPAM="ocamlgraph.2.0.0 cppo.1.6.9" \
-    BASE_ONLY_OPAM="dune.3.8.3 stdlib-shims.0.1.0 ocamlfind.1.9.1 odoc.2.0.2 num.1.4"
+    BASE_ONLY_OPAM="dune.3.8.3 stdlib-shims.0.1.0 ocamlfind.1.9.1 odoc.2.0.2 num.1.4 ppx_optcomp.v0.15.0"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
 ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.2"
diff --git a/dev/ci/scripts/ci-micromega.sh b/dev/ci/scripts/ci-micromega.sh
new file mode 100644
index 000000000000..94aabcdd5dba
--- /dev/null
+++ b/dev/ci/scripts/ci-micromega.sh
@@ -0,0 +1,15 @@
+#!/usr/bin/env bash
+
+set -e
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download micromega
+
+if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
+
+( cd "${CI_BUILD_DIR}/micromega"
+  etc/with-rocq-wrap.sh dune build --root . --only-packages=micromega-plugin @install
+  etc/with-rocq-wrap.sh dune install --root . micromega-plugin --prefix="$CI_INSTALL_DIR"
+)
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 759ae31aa552..c02d06f82d58 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -477,15 +477,15 @@ obtain :math:`-1`. Thus, by Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
     Proof.
     pose (ff := IMPL
       (A isProp
-         {| Flhs := PEadd (PEX 1) (PEmul (PEc 2) (PEX 2));
+         {| Flhs := PEadd (@PEX _ 1) (PEmul (PEc 2) (@PEX _ 2));
             Fop := OpLe; Frhs := PEc 4 |} tt) None
       (IMPL
          (A isProp
-            {| Flhs := PEadd (PEmul (PEc 2) (PEX 1)) (PEX 2);
+            {| Flhs := PEadd (PEmul (PEc 2) (@PEX _ 1)) (@PEX _ 2);
                Fop := OpLe; Frhs := PEc 4 |}
             tt) None
          (A isProp
-            {| Flhs := PEadd (PEX 1) (PEX 2);
+            {| Flhs := PEadd (@PEX _ 1) (@PEX _ 2);
                Fop := OpLt; Frhs := PEc 3 |} tt))
       : BFormula (Formula Q) isProp).