There were two insights that went into making it possible to remove
functional extensionaliy.

1. The insight that went into 4d7999ebb66c1497222d024a1d9f9d0f1ecb2356:
   interp-relatedness implies equivalence.

2. Requiring `f x = v` in the `App`/`LetIn` case of `interp_related_gen`
   et al is essentially saying that, in order to prove
   `interp_related_gen`, we need to materialize an interpretation of the
   function part of applications.  Since interpretation is in general
   highly non-trivial (for `rawexpr`s, `value`s, etc), we must weaken
   this condition.  By instead only requiring `f x == v`, we only
   require being able to manifest *some* function which interprets to
   `v`, a much easier task.  This weakening allows us to prove for each
   interpretation-relation `R` that `(exists e, R e v1 /\ R e v2) <-> v1
   == v2`, i.e., that two interpreted values are equivalent iff there is
   some uninterpreted value which is related to both of them.

   Unfortunately this is not a full specification of
   interpretation-relatedness (we still need to say what it means for a
   particular uninterpreted value to be related to a particular
   interpreted value), and so we still end up doing a lot of work to
   prove various properties.

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

```
   After |  Peak Mem | File Name                                          |   Before |  Peak Mem ||    Change || Change (mem) | % Change | % Change (mem)
---------------------------------------------------------------------------------------------------------------------------------------------------------
9m31.25s | 972156 ko | Total Time / Peak Mem                              | 8m49.94s | 955744 ko || +0m41.31s ||     16412 ko |   +7.79% |         +1.71%
---------------------------------------------------------------------------------------------------------------------------------------------------------
1m14.56s | 859792 ko | Rewriter/Language/UnderLetsProofs                  | 0m46.66s | 767576 ko || +0m27.90s ||     92216 ko |  +59.79% |        +12.01%
0m56.26s | 874108 ko | Rewriter/Rewriter/ProofsCommon                     | 0m48.79s | 869360 ko || +0m07.46s ||      4748 ko |  +15.31% |         +0.54%
0m24.67s | 644504 ko | Rewriter/Language/Wf                               | 0m22.59s | 633232 ko || +0m02.08s ||     11272 ko |   +9.20% |         +1.78%
1m04.38s | 953436 ko | Rewriter/Rewriter/InterpProofs                     | 1m03.09s | 955508 ko || +0m01.28s ||     -2072 ko |   +2.04% |         -0.21%
1m57.29s | 955812 ko | Rewriter/Rewriter/Wf                               | 1m57.19s | 955744 ko || +0m00.09s ||        68 ko |   +0.08% |         +0.00%
0m38.73s | 972156 ko | Rewriter/Rewriter/Examples/SieveOfEratosthenes     | 0m38.15s | 888496 ko || +0m00.57s ||     83660 ko |   +1.52% |         +9.41%
0m34.85s | 811392 ko | Rewriter/Rewriter/Examples                         | 0m34.56s | 811664 ko || +0m00.28s ||      -272 ko |   +0.83% |         -0.03%
0m32.36s | 806524 ko | Rewriter/Rewriter/Examples/PrefixSums              | 0m31.81s | 806696 ko || +0m00.55s ||      -172 ko |   +1.72% |         -0.02%
0m19.35s | 699656 ko | Rewriter/Rewriter/Examples/LiftLetsMap             | 0m19.03s | 696620 ko || +0m00.32s ||      3036 ko |   +1.68% |         +0.43%
0m18.74s | 612996 ko | Rewriter/Language/Inversion                        | 0m18.73s | 612420 ko || +0m00.00s ||       576 ko |   +0.05% |         +0.09%
0m15.07s | 686200 ko | Rewriter/Rewriter/Examples/Plus0Tree               | 0m14.93s | 685612 ko || +0m00.14s ||       588 ko |   +0.93% |         +0.08%
0m14.94s | 685332 ko | Rewriter/Rewriter/Examples/UnderLetsPlus0          | 0m14.75s | 685192 ko || +0m00.18s ||       140 ko |   +1.28% |         +0.02%
0m14.41s | 731276 ko | Rewriter/Demo                                      | 0m14.43s | 743012 ko || -0m00.01s ||    -11736 ko |   -0.13% |         -1.57%
0m13.15s | 637292 ko | Rewriter/Language/IdentifiersLibraryProofs         | 0m13.17s | 640980 ko || -0m00.01s ||     -3688 ko |   -0.15% |         -0.57%
0m06.79s | 503412 ko | Rewriter/Util/ListUtil                             | 0m06.56s | 501208 ko || +0m00.23s ||      2204 ko |   +3.50% |         +0.43%
0m04.58s | 527384 ko | Rewriter/Language/IdentifiersBasicLibrary          | 0m04.57s | 527564 ko || +0m00.00s ||      -180 ko |   +0.21% |         -0.03%
0m01.77s | 577488 ko | Rewriter/Rewriter/Examples/PerfTesting/Harness     | 0m01.87s | 577872 ko || -0m00.10s ||      -384 ko |   -5.34% |         -0.06%
0m01.72s | 457916 ko | Rewriter/Util/NatUtil                              | 0m01.70s | 457296 ko || +0m00.02s ||       620 ko |   +1.17% |         +0.13%
0m01.55s | 521092 ko | Rewriter/Language/IdentifiersLibrary               | 0m01.58s | 519796 ko || -0m00.03s ||      1296 ko |   -1.89% |         +0.24%
0m01.34s | 518212 ko | Rewriter/Rewriter/Rewriter                         | 0m01.37s | 515708 ko || -0m00.03s ||      2504 ko |   -2.18% |         +0.48%
0m01.22s | 518556 ko | Rewriter/Rewriter/Reify                            | 0m01.22s | 517588 ko || +0m00.00s ||       968 ko |   +0.00% |         +0.18%
0m01.18s | 477976 ko | Rewriter/Language/Language                         | 0m01.15s | 477124 ko || +0m00.03s ||       852 ko |   +2.60% |         +0.17%
0m01.14s | 539084 ko | Rewriter/Rewriter/AllTactics                       | 0m01.11s | 537084 ko || +0m00.02s ||      2000 ko |   +2.70% |         +0.37%
0m01.13s | 444328 ko | Rewriter/Util/ListUtil/Forall                      | 0m01.04s | 445248 ko || +0m00.08s ||      -920 ko |   +8.65% |         -0.20%
0m00.95s | 523516 ko | Rewriter/Rewriter/ProofsCommonTactics              | 0m00.95s | 520348 ko || +0m00.00s ||      3168 ko |   +0.00% |         +0.60%
0m00.90s | 506864 ko | Rewriter/Language/IdentifiersGenerate              | 0m00.81s | 505404 ko || +0m00.08s ||      1460 ko |  +11.11% |         +0.28%
0m00.90s | 558172 ko | Rewriter/Rewriter/Examples/PerfTesting/All         | 0m00.87s | 560168 ko || +0m00.03s ||     -1996 ko |   +3.44% |         -0.35%
0m00.89s | 532984 ko | Rewriter/Rewriter/Examples/PerfTesting/Settings    | 0m00.87s | 534512 ko || +0m00.02s ||     -1528 ko |   +2.29% |         -0.28%
0m00.83s | 507180 ko | Rewriter/Language/IdentifiersGenerateProofs        | 0m00.84s | 506900 ko || -0m00.01s ||       280 ko |   -1.19% |         +0.05%
0m00.82s | 530880 ko | Rewriter/Util/plugins/RewriterBuild                | 0m00.79s | 529620 ko || +0m00.02s ||      1260 ko |   +3.79% |         +0.23%
0m00.81s | 530028 ko | Rewriter/Util/plugins/RewriterBuildRegistry        | 0m00.78s | 528980 ko || +0m00.03s ||      1048 ko |   +3.84% |         +0.19%
0m00.78s | 533476 ko | Rewriter/Util/plugins/RewriterBuildRegistryImports | 0m00.80s | 531528 ko || -0m00.02s ||      1948 ko |   -2.50% |         +0.36%
0m00.70s | 458240 ko | Rewriter/Util/Bool/Reflect                         | 0m00.71s | 457920 ko || -0m00.01s ||       320 ko |   -1.40% |         +0.06%
0m00.56s | 473820 ko | Rewriter/Language/IdentifiersBasicGenerate         | 0m00.59s | 473848 ko || -0m00.02s ||       -28 ko |   -5.08% |         -0.00%
0m00.48s | 449072 ko | Rewriter/Util/MSetPositive/Facts                   | 0m00.47s | 449132 ko || +0m00.01s ||       -60 ko |   +2.12% |         -0.01%
0m00.46s | 463164 ko | Rewriter/Language/UnderLets                        | 0m00.46s | 462804 ko || +0m00.00s ||       360 ko |   +0.00% |         +0.07%
0m00.31s | 400688 ko | Rewriter/Language/PreLemmas                        | 0m00.32s | 398084 ko || -0m00.01s ||      2604 ko |   -3.12% |         +0.65%
0m00.27s | 312208 ko | Rewriter/Util/Option                               | 0m00.26s | 311880 ko || +0m00.01s ||       328 ko |   +3.84% |         +0.10%
0m00.18s | 339048 ko | Rewriter/Util/OptionList                           | 0m00.17s | 338844 ko || +0m00.00s ||       204 ko |   +5.88% |         +0.06%
0m00.09s | 202332 ko | Rewriter/Util/ListUtil/SetoidList                  | 0m00.12s | 202224 ko || -0m00.03s ||       108 ko |  -25.00% |         +0.05%
0m00.08s | 133832 ko | Rewriter/Util/Bool                                 | 0m00.08s | 116804 ko || +0m00.00s ||     17028 ko |   +0.00% |        +14.57%
0m00.04s |  57244 ko | Rewriter/Util/Tactics/Contains                     |   N/A    |    N/A    || +0m00.04s ||     57244 ko |        ∞ |              ∞
0m00.03s |  58744 ko | Rewriter/Util/Tactics/SetoidSubst                  |   N/A    |    N/A    || +0m00.03s ||     58744 ko |        ∞ |              ∞

```
</p>