Global Strategy -1000 [UnderLets.to_expr]. (#75)

We will need this for using `UnderLets.to_expr` in reification

<details><summary>Timing Diff</summary>
<p>

```
    After |   Peak Mem | File Name                                                     |    Before |   Peak Mem ||    Change || Change (mem) | % Change | % Change (mem)
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
10m00.73s | 1401132 ko | Total Time / Peak Mem                                         | 10m01.39s | 1401188 ko || -0m00.66s ||       -56 ko |   -0.11% |         -0.00%
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
 1m49.70s | 1142680 ko | Rewriter/Rewriter/Wf.vo                                       |  1m50.19s | 1142852 ko || -0m00.48s ||      -172 ko |   -0.44% |         -0.01%
 0m59.71s |  728232 ko | Rewriter/Language/UnderLetsProofs.vo                          |  0m59.61s |  727760 ko || +0m00.10s ||       472 ko |   +0.16% |         +0.06%
 0m54.69s | 1114640 ko | Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.vo         |  0m54.64s | 1114536 ko || +0m00.04s ||       104 ko |   +0.09% |         +0.00%
 0m54.36s | 1401132 ko | Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.vo |  0m54.15s | 1401188 ko || +0m00.21s ||       -56 ko |   +0.38% |         -0.00%
 0m53.42s | 1059016 ko | Rewriter/Rewriter/Examples.vo                                 |  0m53.27s | 1058944 ko || +0m00.14s ||        72 ko |   +0.28% |         +0.00%
 0m52.22s |  941700 ko | Rewriter/Rewriter/InterpProofs.vo                             |  0m52.42s |  941852 ko || -0m00.20s ||      -152 ko |   -0.38% |         -0.01%
 0m48.30s |  790584 ko | Rewriter/Rewriter/ProofsCommon.vo                             |  0m48.53s |  791528 ko || -0m00.23s ||      -944 ko |   -0.47% |         -0.11%
 0m29.51s |  923852 ko | Rewriter/Rewriter/Examples/PrefixSums.vo                      |  0m29.65s |  923840 ko || -0m00.13s ||        12 ko |   -0.47% |         +0.00%
 0m26.67s |  679988 ko | Rewriter/Language/Wf.vo                                       |  0m26.62s |  679904 ko || +0m00.05s ||        84 ko |   +0.18% |         +0.01%
 0m23.43s |  886412 ko | Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.vo           |  0m23.44s |  886340 ko || -0m00.01s ||        72 ko |   -0.04% |         +0.00%
 0m17.70s |  574524 ko | Rewriter/Language/Inversion.vo                                |  0m17.71s |  574636 ko || -0m00.01s ||      -112 ko |   -0.05% |         -0.01%
 0m15.87s |  734496 ko | Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.vo      |  0m15.82s |  734664 ko || +0m00.04s ||      -168 ko |   +0.31% |         -0.02%
 0m11.88s |  636892 ko | Rewriter/Demo.vo                                              |  0m11.91s |  636984 ko || -0m00.02s ||       -92 ko |   -0.25% |         -0.01%
 0m08.84s |  506792 ko | Rewriter/Language/IdentifiersLibraryProofs.vo                 |  0m08.73s |  506796 ko || +0m00.10s ||        -4 ko |   +1.26% |         -0.00%
 0m05.90s |  455204 ko | Rewriter/Util/ListUtil.vo                                     |  0m05.93s |  455216 ko || -0m00.02s ||       -12 ko |   -0.50% |         -0.00%
 0m04.04s |  469224 ko | Rewriter/Language/IdentifiersBasicLibrary.vo                  |  0m04.05s |  469108 ko || -0m00.00s ||       116 ko |   -0.24% |         +0.02%
 0m02.42s |  423132 ko | Rewriter/Util/Bool/Reflect.vo                                 |  0m02.48s |  423280 ko || -0m00.06s ||      -148 ko |   -2.41% |         -0.03%
 0m01.47s |  409872 ko | Rewriter/Util/ListUtil/Forall.vo                              |  0m01.47s |  409924 ko || +0m00.00s ||       -52 ko |   +0.00% |         -0.01%
 0m01.24s |  466968 ko | Rewriter/Language/IdentifiersLibrary.vo                       |  0m01.24s |  466960 ko || +0m00.00s ||         8 ko |   +0.00% |         +0.00%
 0m01.24s |  409320 ko | Rewriter/Rewriter/Examples/PerfTesting/Harness.vo             |  0m01.23s |  409188 ko || +0m00.01s ||       132 ko |   +0.81% |         +0.03%
 0m00.93s |  413512 ko | Rewriter/Util/NatUtil.vo                                      |  0m00.93s |  413564 ko || +0m00.00s ||       -52 ko |   +0.00% |         -0.01%
 0m00.91s |  465564 ko | Rewriter/Rewriter/Rewriter.vo                                 |  0m00.99s |  465596 ko || -0m00.07s ||       -32 ko |   -8.08% |         -0.00%
 0m00.90s |  475652 ko | Rewriter/Rewriter/Reify.vo                                    |  0m00.92s |  475652 ko || -0m00.02s ||         0 ko |   -2.17% |         +0.00%
 0m00.85s |  444856 ko | Rewriter/Language/Language.vo                                 |  0m00.86s |  444800 ko || -0m00.01s ||        56 ko |   -1.16% |         +0.01%
 0m00.74s |  488860 ko | Rewriter/Rewriter/AllTactics.vo                               |  0m00.82s |  488904 ko || -0m00.07s ||       -44 ko |   -9.75% |         -0.00%
 0m00.73s |  408496 ko | Rewriter/Rewriter/Examples/PerfTesting/Sample.vo              |  0m00.76s |  408600 ko || -0m00.03s ||      -104 ko |   -3.94% |         -0.02%
 0m00.65s |  379960 ko | Rewriter/Util/Decidable.vo                                    |  0m00.61s |  379904 ko || +0m00.04s ||        56 ko |   +6.55% |         +0.01%
 0m00.59s |  456852 ko | Rewriter/Language/IdentifiersGenerate.vo                      |  0m00.54s |  456948 ko || +0m00.04s ||       -96 ko |   +9.25% |         -0.02%
 0m00.59s |  471464 ko | Rewriter/Rewriter/ProofsCommonTactics.vo                      |  0m00.61s |  471260 ko || -0m00.02s ||       204 ko |   -3.27% |         +0.04%
 0m00.57s |  480560 ko | Rewriter/Util/plugins/RewriterBuildRegistry.vo                |  0m00.49s |  480300 ko || +0m00.07s ||       260 ko |  +16.32% |         +0.05%
 0m00.53s |  457920 ko | Rewriter/Language/IdentifiersGenerateProofs.vo                |  0m00.47s |  457832 ko || +0m00.06s ||        88 ko |  +12.76% |         +0.01%
 0m00.53s |  479060 ko | Rewriter/Util/plugins/RewriterBuildRegistryImports.vo         |  0m00.56s |  478932 ko || -0m00.03s ||       128 ko |   -5.35% |         +0.02%
 0m00.50s |  480536 ko | Rewriter/Util/plugins/RewriterBuild.vo                        |  0m00.45s |  480496 ko || +0m00.04s ||        40 ko |  +11.11% |         +0.00%
 0m00.49s |  441316 ko | Rewriter/Language/IdentifiersBasicGenerate.vo                 |  0m00.49s |  441204 ko || +0m00.00s ||       112 ko |   +0.00% |         +0.02%
 0m00.47s |  482464 ko | Rewriter/Rewriter/Examples/PerfTesting/Settings.vo            |  0m00.47s |  482384 ko || +0m00.00s ||        80 ko |   +0.00% |         +0.01%
 0m00.42s |  381876 ko | Rewriter/Util/Sum.vo                                          |  0m00.43s |  381932 ko || -0m00.01s ||       -56 ko |   -2.32% |         -0.01%
 0m00.41s |  424548 ko | Rewriter/Language/Reify.vo                                    |  0m00.36s |  424428 ko || +0m00.04s ||       120 ko |  +13.88% |         +0.02%
 0m00.33s |  412068 ko | Rewriter/Util/Strings/ParseArithmetic.vo                      |  0m00.35s |  412208 ko || -0m00.01s ||      -140 ko |   -5.71% |         -0.03%
 0m00.29s |  336492 ko | Rewriter/Util/MSetPositive/Equality.vo                        |  0m00.30s |  336560 ko || -0m00.01s ||       -68 ko |   -3.33% |         -0.02%
 0m00.29s |  372040 ko | Rewriter/Util/MSetPositive/Facts.vo                           |  0m00.33s |  372168 ko || -0m00.04s ||      -128 ko |  -12.12% |         -0.03%
 0m00.28s |  387808 ko | Rewriter/Language/UnderLets.vo                                |  0m00.33s |  387632 ko || -0m00.04s ||       176 ko |  -15.15% |         +0.04%
 0m00.25s |  307788 ko | Rewriter/Language/PreLemmas.vo                                |  0m00.28s |  307888 ko || -0m00.03s ||      -100 ko |  -10.71% |         -0.03%
 0m00.25s |  345464 ko | Rewriter/Util/ListUtil/SetoidList.vo                          |  0m00.24s |  345480 ko || +0m00.01s ||       -16 ko |   +4.16% |         -0.00%
 0m00.23s |  314084 ko | Rewriter/Util/Option.vo                                       |  0m00.26s |  314124 ko || -0m00.03s ||       -40 ko |  -11.53% |         -0.01%
 0m00.23s |  367756 ko | Rewriter/Util/Strings/String.vo                               |  0m00.26s |  367772 ko || -0m00.03s ||       -16 ko |  -11.53% |         -0.00%
 0m00.21s |  323684 ko | Rewriter/Language/UnderLetsCacheProofs.vo                     |  0m00.24s |  323216 ko || -0m00.03s ||       468 ko |  -12.50% |         +0.14%
 0m00.19s |  303140 ko | Rewriter/Util/FMapPositive/Equality.vo                        |  0m00.19s |  303024 ko || +0m00.00s ||       116 ko |   +0.00% |         +0.03%
 0m00.18s |  267900 ko | Rewriter/Util/Strings/Parse/Common.vo                         |  0m00.18s |  268108 ko || +0m00.00s ||      -208 ko |   +0.00% |         -0.07%
 0m00.17s |  251988 ko | Rewriter/Util/Strings/Decimal.vo                              |  0m00.13s |  252092 ko || +0m00.04s ||      -104 ko |  +30.76% |         -0.04%
 0m00.16s |  209704 ko | Rewriter/Util/Strings/Ascii.vo                                |  0m00.13s |  209556 ko || +0m00.03s ||       148 ko |  +23.07% |         +0.07%
 0m00.14s |  263380 ko | Rewriter/Util/Prod.vo                                         |  0m00.13s |  263480 ko || +0m00.01s ||      -100 ko |   +7.69% |         -0.03%
 0m00.13s |  257012 ko | Rewriter/Util/OptionList.vo                                   |  0m00.19s |  257132 ko || -0m00.06s ||      -120 ko |  -31.57% |         -0.04%
 0m00.11s |  115068 ko | Rewriter/Language/Pre.vo                                      |  0m00.09s |  114828 ko || +0m00.02s ||       240 ko |  +22.22% |         +0.20%
 0m00.11s |  195496 ko | Rewriter/Util/PrimitiveProd.vo                                |  0m00.11s |  195572 ko || +0m00.00s ||       -76 ko |   +0.00% |         -0.03%
 0m00.11s |  220420 ko | Rewriter/Util/Sigma.vo                                        |  0m00.14s |  220324 ko || -0m00.03s ||        96 ko |  -21.42% |         +0.04%
 0m00.10s |  111776 ko | Rewriter/Util/PrimitiveHList.vo                               |  0m00.08s |  111708 ko || +0m00.02s ||        68 ko |  +25.00% |         +0.06%
 0m00.10s |  161712 ko | Rewriter/Util/PrimitiveSigma.vo                               |  0m00.11s |  161512 ko || -0m00.00s ||       200 ko |   -9.09% |         +0.12%
 0m00.09s |  113096 ko | Rewriter/Language/PreCommon.vo                                |  0m00.07s |  112976 ko || +0m00.01s ||       120 ko |  +28.57% |         +0.10%
 0m00.08s |  114432 ko | Rewriter/Util/Sigma/Related.vo                                |  0m00.05s |  114516 ko || +0m00.03s ||       -84 ko |  +60.00% |         -0.07%
 0m00.08s |   30616 ko | Rewriter/Util/plugins/rewriter_build.cmx                      |  0m00.08s |   30592 ko || +0m00.00s ||        24 ko |   +0.00% |         +0.07%
 0m00.07s |  129832 ko | Rewriter/Util/Bool.vo                                         |  0m00.07s |  129668 ko || +0m00.00s ||       164 ko |   +0.00% |         +0.12%
 0m00.07s |  136472 ko | Rewriter/Util/Equality.vo                                     |  0m00.07s |  136508 ko || +0m00.00s ||       -36 ko |   +0.00% |         -0.02%
 0m00.07s |   74068 ko | Rewriter/Util/Tactics/BreakMatch.vo                           |  0m00.06s |   74300 ko || +0m00.01s ||      -232 ko |  +16.66% |         -0.31%
 0m00.07s |   95092 ko | Rewriter/Util/Tactics/RewriteHyp.vo                           |  0m00.03s |   95280 ko || +0m00.04s ||      -188 ko | +133.33% |         -0.19%
 0m00.07s |   77992 ko | Rewriter/Util/Tactics2/ReplaceByPattern.vo                    |  0m00.03s |   77956 ko || +0m00.04s ||        36 ko | +133.33% |         +0.04%
 0m00.06s |  131564 ko | Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.vo   |  0m00.09s |  131492 ko || -0m00.03s ||        72 ko |  -33.33% |         +0.05%
 0m00.06s |   99512 ko | Rewriter/Util/Logic/ExistsEqAnd.vo                            |  0m00.05s |   99488 ko || +0m00.00s ||        24 ko |  +19.99% |         +0.02%
 0m00.06s |   77760 ko | Rewriter/Util/Tactics2/Constr.vo                              |  0m00.06s |   77700 ko || +0m00.00s ||        60 ko |   +0.00% |         +0.07%
 0m00.06s |   77868 ko | Rewriter/Util/Tactics2/DecomposeLambda.vo                     |  0m00.06s |   77904 ko || +0m00.00s ||       -36 ko |   +0.00% |         -0.04%
 0m00.06s |   26956 ko | Rewriter/Util/plugins/rewriter_build_plugin.cmx               |  0m00.08s |   26916 ko || -0m00.02s ||        40 ko |  -25.00% |         +0.14%
 0m00.06s |   52920 ko | Rewriter/Util/plugins/rewriter_build_plugin.cmxa              |  0m00.02s |   52560 ko || +0m00.03s ||       360 ko | +199.99% |         +0.68%
 0m00.06s |   21100 ko | Rewriter/Util/plugins/rewriter_build_plugin.cmxs              |  0m00.06s |   21132 ko || +0m00.00s ||       -32 ko |   +0.00% |         -0.15%
 0m00.05s |   70096 ko | Rewriter/Util/InductiveHList.vo                               |  0m00.01s |   70200 ko || +0m00.04s ||      -104 ko | +400.00% |         -0.14%
 0m00.05s |   69008 ko | Rewriter/Util/Tactics/CPSId.vo                                |  0m00.05s |   68692 ko || +0m00.00s ||       316 ko |   +0.00% |         +0.46%
 0m00.05s |   70984 ko | Rewriter/Util/Tactics/SpecializeAllWays.vo                    |  0m00.03s |   71040 ko || +0m00.02s ||       -56 ko |  +66.66% |         -0.07%
 0m00.05s |   72196 ko | Rewriter/Util/Tactics/SplitInContext.vo                       |  0m00.01s |   72016 ko || +0m00.04s ||       180 ko | +400.00% |         +0.24%
 0m00.05s |   77288 ko | Rewriter/Util/Tactics2/Array.vo                               |  0m00.05s |   77364 ko || +0m00.00s ||       -76 ko |   +0.00% |         -0.09%
 0m00.05s |   77384 ko | Rewriter/Util/Tactics2/Constr/Unsafe/MakeAbbreviations.vo     |  0m00.04s |   77384 ko || +0m00.01s ||         0 ko |  +25.00% |         +0.00%
 0m00.05s |   77548 ko | Rewriter/Util/Tactics2/Head.vo                                |  0m00.03s |   77444 ko || +0m00.02s ||       104 ko |  +66.66% |         +0.13%
 0m00.05s |   77628 ko | Rewriter/Util/Tactics2/Ident.vo                               |  0m00.07s |   77656 ko || -0m00.02s ||       -28 ko |  -28.57% |         -0.03%
 0m00.05s |   77392 ko | Rewriter/Util/Tactics2/List.vo                                |  0m00.04s |   77372 ko || +0m00.01s ||        20 ko |  +25.00% |         +0.02%
 0m00.05s |   77408 ko | Rewriter/Util/Tactics2/Option.vo                              |  0m00.03s |   77348 ko || +0m00.02s ||        60 ko |  +66.66% |         +0.07%
 0m00.05s |   77452 ko | Rewriter/Util/Tactics2/String.vo                              |  0m00.05s |   77440 ko || +0m00.00s ||        12 ko |   +0.00% |         +0.01%
 0m00.05s |   68912 ko | Rewriter/Util/TypeList.vo                                     |  0m00.03s |   68912 ko || +0m00.02s ||         0 ko |  +66.66% |         +0.00%
 0m00.04s |   75740 ko | Rewriter/Util/Bool/Equality.vo                                |  0m00.03s |   75740 ko || +0m00.01s ||         0 ko |  +33.33% |         +0.00%
 0m00.04s |   78652 ko | Rewriter/Util/Comparison.vo                                   |  0m00.02s |   78552 ko || +0m00.02s ||       100 ko | +100.00% |         +0.12%
 0m00.04s |   84316 ko | Rewriter/Util/Logic/ProdForall.vo                             |  0m00.04s |   84472 ko || +0m00.00s ||      -156 ko |   +0.00% |         -0.18%
 0m00.04s |   77708 ko | Rewriter/Util/Tactics/DestructHead.vo                         |  0m00.02s |   77768 ko || +0m00.02s ||       -60 ko | +100.00% |         -0.07%
 0m00.04s |   71032 ko | Rewriter/Util/Tactics/FindHyp.vo                              |  0m00.05s |   71236 ko || -0m00.01s ||      -204 ko |  -20.00% |         -0.28%
 0m00.04s |   70716 ko | Rewriter/Util/Tactics/Head.vo                                 |  0m00.03s |   70776 ko || +0m00.01s ||       -60 ko |  +33.33% |         -0.08%
 0m00.04s |   67900 ko | Rewriter/Util/Tactics/SetoidSubst.vo                          |  0m00.02s |   68052 ko || +0m00.02s ||      -152 ko | +100.00% |         -0.22%
 0m00.04s |   71608 ko | Rewriter/Util/Tactics/UniquePose.vo                           |  0m00.03s |   71708 ko || +0m00.01s ||      -100 ko |  +33.33% |         -0.13%
 0m00.04s |   78696 ko | Rewriter/Util/Tactics2/FixNotationsForPerformance.vo          |  0m00.03s |   78712 ko || +0m00.01s ||       -16 ko |  +33.33% |         -0.02%
 0m00.04s |   77644 ko | Rewriter/Util/Tactics2/HeadReference.vo                       |  0m00.05s |   77656 ko || -0m00.01s ||       -12 ko |  -20.00% |         -0.01%
 0m00.04s |   77348 ko | Rewriter/Util/Tactics2/Iterate.vo                             |  0m00.05s |   77332 ko || -0m00.01s ||        16 ko |  -20.00% |         +0.02%
 0m00.04s |   77348 ko | Rewriter/Util/Tactics2/Message.vo                             |  0m00.05s |   77424 ko || -0m00.01s ||       -76 ko |  -20.00% |         -0.09%
 0m00.04s |   19716 ko | Rewriter/Util/plugins/definition_by_tactic_plugin.cmxs        |  0m00.02s |   19724 ko || +0m00.02s ||        -8 ko | +100.00% |         -0.04%
 0m00.04s |   52712 ko | Rewriter/Util/plugins/ltac2_extra_plugin.cmxa                 |  0m00.04s |   52436 ko || +0m00.00s ||       276 ko |   +0.00% |         +0.52%
 0m00.04s |   53276 ko | Rewriter/Util/plugins/strategy_tactic_plugin.cmxa             |  0m00.04s |   52788 ko || +0m00.00s ||       488 ko |   +0.00% |         +0.92%
 0m00.03s |   77720 ko | Rewriter/Util/CPSNotations.vo                                 |  0m00.07s |   77832 ko || -0m00.04s ||      -112 ko |  -57.14% |         -0.14%
 0m00.03s |   85764 ko | Rewriter/Util/IffT.vo                                         |  0m00.03s |   85896 ko || +0m00.00s ||      -132 ko |   +0.00% |         -0.15%
 0m00.03s |   98240 ko | Rewriter/Util/LetIn.vo                                        |  0m00.03s |   98092 ko || +0m00.00s ||       148 ko |   +0.00% |         +0.15%
 0m00.03s |   82412 ko | Rewriter/Util/Notations.vo                                    |  0m00.02s |   82316 ko || +0m00.00s ||        96 ko |  +49.99% |         +0.11%
 0m00.03s |   87472 ko | Rewriter/Util/Pointed.vo                                      |  0m00.05s |   87468 ko || -0m00.02s ||         4 ko |  -40.00% |         +0.00%
 0m00.03s |   69236 ko | Rewriter/Util/Tactics/CacheTerm.vo                            |  0m00.04s |   69284 ko || -0m00.01s ||       -48 ko |  -25.00% |         -0.06%
 0m00.03s |   66848 ko | Rewriter/Util/Tactics/ConstrFail.vo                           |  0m00.04s |   66824 ko || -0m00.01s ||        24 ko |  -25.00% |         +0.03%
 0m00.03s |   66876 ko | Rewriter/Util/Tactics/Contains.vo                             |  0m00.03s |   66808 ko || +0m00.00s ||        68 ko |   +0.00% |         +0.10%
 0m00.03s |   75772 ko | Rewriter/Util/Tactics/DebugPrint.vo                           |  0m00.03s |   75796 ko || +0m00.00s ||       -24 ko |   +0.00% |         -0.03%
 0m00.03s |   71144 ko | Rewriter/Util/Tactics/DoWithHyp.vo                            |  0m00.04s |   71204 ko || -0m00.01s ||       -60 ko |  -25.00% |         -0.08%
 0m00.03s |   66840 ko | Rewriter/Util/Tactics/EvarNormalize.vo                        |  0m00.04s |   66924 ko || -0m00.01s ||       -84 ko |  -25.00% |         -0.12%
 0m00.03s |   66820 ko | Rewriter/Util/Tactics/GetGoal.vo                              |  0m00.03s |   66756 ko || +0m00.00s ||        64 ko |   +0.00% |         +0.09%
 0m00.03s |   71152 ko | Rewriter/Util/Tactics/HeadUnderBinders.vo                     |  0m00.03s |   71044 ko || +0m00.00s ||       108 ko |   +0.00% |         +0.15%
 0m00.03s |   66900 ko | Rewriter/Util/Tactics/Not.vo                                  |  0m00.02s |   66824 ko || +0m00.00s ||        76 ko |  +49.99% |         +0.11%
 0m00.03s |   70940 ko | Rewriter/Util/Tactics/RunTacticAsConstr.vo                    |  0m00.01s |   71096 ko || +0m00.01s ||      -156 ko | +199.99% |         -0.21%
 0m00.03s |   66732 ko | Rewriter/Util/Tactics/Test.vo                                 |  0m00.05s |   66716 ko || -0m00.02s ||        16 ko |  -40.00% |         +0.02%
 0m00.03s |   67784 ko | Rewriter/Util/Tactics/TransparentAssert.vo                    |  0m00.02s |   67560 ko || +0m00.00s ||       224 ko |  +49.99% |         +0.33%
 0m00.03s |   77464 ko | Rewriter/Util/Tactics2/Char.vo                                |  0m00.04s |   77428 ko || -0m00.01s ||        36 ko |  -25.00% |         +0.04%
 0m00.03s |   77472 ko | Rewriter/Util/Tactics2/InFreshContext.vo                      |  0m00.04s |   77504 ko || -0m00.01s ||       -32 ko |  -25.00% |         -0.04%
 0m00.03s |   77424 ko | Rewriter/Util/Tactics2/Ltac1.vo                               |  0m00.05s |   77320 ko || -0m00.02s ||       104 ko |  -40.00% |         +0.13%
 0m00.03s |   77356 ko | Rewriter/Util/Tactics2/Notations.vo                           |  0m00.04s |   77480 ko || -0m00.01s ||      -124 ko |  -25.00% |         -0.16%
 0m00.03s |   52900 ko | Rewriter/Util/plugins/definition_by_tactic_plugin.cmxa        |  0m00.04s |   53200 ko || -0m00.01s ||      -300 ko |  -25.00% |         -0.56%
 0m00.03s |   20384 ko | Rewriter/Util/plugins/inductive_from_elim.cmi                 |  0m00.02s |   20148 ko || +0m00.00s ||       236 ko |  +49.99% |         +1.17%
 0m00.03s |   28460 ko | Rewriter/Util/plugins/inductive_from_elim.cmx                 |  0m00.04s |   28484 ko || -0m00.01s ||       -24 ko |  -25.00% |         -0.08%
 0m00.03s |   24220 ko | Rewriter/Util/plugins/inductive_from_elim_plugin.cmx          |  0m00.03s |   24008 ko || +0m00.00s ||       212 ko |   +0.00% |         +0.88%
 0m00.03s |   19540 ko | Rewriter/Util/plugins/inductive_from_elim_plugin.cmxs         |  0m00.02s |   19688 ko || +0m00.00s ||      -148 ko |  +49.99% |         -0.75%
 0m00.03s |   19632 ko | Rewriter/Util/plugins/ltac2_extra_plugin.cmxs                 |  0m00.01s |   19756 ko || +0m00.01s ||      -124 ko | +199.99% |         -0.62%
 0m00.02s |   76936 ko | Rewriter/Util/FixCoqMistakes.vo                               |  0m00.03s |   76976 ko || -0m00.00s ||       -40 ko |  -33.33% |         -0.05%
 0m00.02s |   95764 ko | Rewriter/Util/HProp.vo                                        |  0m00.05s |   95824 ko || -0m00.03s ||       -60 ko |  -60.00% |         -0.06%
 0m00.02s |   67804 ko | Rewriter/Util/Isomorphism.vo                                  |  0m00.03s |   67652 ko || -0m00.00s ||       152 ko |  -33.33% |         +0.22%
 0m00.02s |   70672 ko | Rewriter/Util/Tactics/AssertSucceedsPreserveError.vo          |  0m00.05s |   70804 ko || -0m00.03s ||      -132 ko |  -60.00% |         -0.18%
 0m00.02s |   66968 ko | Rewriter/Util/Tactics/ClearFree.vo                            |  0m00.02s |   66884 ko || +0m00.00s ||        84 ko |   +0.00% |         +0.12%
 0m00.02s |   72272 ko | Rewriter/Util/Tactics/DestructHyps.vo                         |  0m00.05s |   72296 ko || -0m00.03s ||       -24 ko |  -60.00% |         -0.03%
 0m00.02s |   71536 ko | Rewriter/Util/Tactics/SpecializeBy.vo                         |  0m00.03s |   71440 ko || -0m00.00s ||        96 ko |  -33.33% |         +0.13%
 0m00.02s |   66928 ko | Rewriter/Util/Tactics/SubstEvars.vo                           |  0m00.02s |   66760 ko || +0m00.00s ||       168 ko |   +0.00% |         +0.25%
 0m00.02s |   67116 ko | Rewriter/Util/Tactics/WarnIfGoalsRemain.vo                    |  0m00.03s |   66940 ko || -0m00.00s ||       176 ko |  -33.33% |         +0.26%
 0m00.02s |   77280 ko | Rewriter/Util/Tactics2/Proj.vo                                |  0m00.03s |   77468 ko || -0m00.00s ||      -188 ko |  -33.33% |         -0.24%
 0m00.02s |   20456 ko | Rewriter/Util/plugins/definition_by_tactic.cmi                |  0m00.02s |   20608 ko || +0m00.00s ||      -152 ko |   +0.00% |         -0.73%
 0m00.02s |   26476 ko | Rewriter/Util/plugins/definition_by_tactic.cmx                |  0m00.03s |   26380 ko || -0m00.00s ||        96 ko |  -33.33% |         +0.36%
 0m00.02s |   22920 ko | Rewriter/Util/plugins/ltac2_extra.cmx                         |  0m00.03s |   22996 ko || -0m00.00s ||       -76 ko |  -33.33% |         -0.33%
 0m00.02s |   19356 ko | Rewriter/Util/plugins/rewriter_build.cmi                      |  0m00.02s |   19160 ko || +0m00.00s ||       196 ko |   +0.00% |         +1.02%
 0m00.02s |   23348 ko | Rewriter/Util/plugins/strategy_tactic_plugin.cmx              |  0m00.02s |   23268 ko || +0m00.00s ||        80 ko |   +0.00% |         +0.34%
 0m00.02s |   19312 ko | Rewriter/Util/plugins/strategy_tactic_plugin.cmxs             |  0m00.03s |   19272 ko || -0m00.00s ||        40 ko |  -33.33% |         +0.20%
 0m00.01s |   66880 ko | Rewriter/Util/Tactics/PrintContext.vo                         |  0m00.02s |   66948 ko || -0m00.01s ||       -68 ko |  -50.00% |         -0.10%
 0m00.01s |   67196 ko | Rewriter/Util/Tactics/PrintGoal.vo                            |  0m00.02s |   67032 ko || -0m00.01s ||       164 ko |  -50.00% |         +0.24%
 0m00.01s |   77200 ko | Rewriter/Util/plugins/Ltac2Extra.vo                           |  0m00.04s |   77196 ko || -0m00.03s ||         4 ko |  -75.00% |         +0.00%
 0m00.01s |   66732 ko | Rewriter/Util/plugins/StrategyTactic.vo                       |  0m00.02s |   66716 ko || -0m00.01s ||        16 ko |  -50.00% |         +0.02%
 0m00.01s |   25396 ko | Rewriter/Util/plugins/definition_by_tactic_plugin.cmx         |  0m00.02s |   25316 ko || -0m00.01s ||        80 ko |  -50.00% |         +0.31%
 0m00.01s |   53388 ko | Rewriter/Util/plugins/inductive_from_elim_plugin.cmxa         |  0m00.02s |   52852 ko || -0m00.01s ||       536 ko |  -50.00% |         +1.01%
 0m00.01s |   17176 ko | Rewriter/Util/plugins/ltac2_extra.cmi                         |  0m00.02s |   17280 ko || -0m00.01s ||      -104 ko |  -50.00% |         -0.60%
 0m00.01s |   20184 ko | Rewriter/Util/plugins/ltac2_extra_plugin.cmx                  |  0m00.02s |   20032 ko || -0m00.01s ||       152 ko |  -50.00% |         +0.75%
 0m00.01s |   19200 ko | Rewriter/Util/plugins/strategy_tactic.cmi                     |  0m00.01s |   19248 ko || +0m00.00s ||       -48 ko |   +0.00% |         -0.24%
 0m00.01s |   22632 ko | Rewriter/Util/plugins/strategy_tactic.cmx                     |  0m00.02s |   22684 ko || -0m00.01s ||       -52 ko |  -50.00% |         -0.22%
 0m00.00s |   66280 ko | Rewriter/Util/GlobalSettings.vo                               |  0m00.02s |   66200 ko || -0m00.02s ||        80 ko | -100.00% |         +0.12%
 0m00.00s |   66712 ko | Rewriter/Util/Tactics/SetEvars.vo                             |  0m00.01s |   66844 ko || -0m00.01s ||      -132 ko | -100.00% |         -0.19%

```
</p>
</details>

src/Rewriter/Language/UnderLets.v

@@ -263,4 +263,5 @@ Module Compilers.
     End reify.
   End UnderLets.
   Export UnderLets.Notations.
+  Global Strategy -1000 [UnderLets.to_expr].
 End Compilers.