perf: `mkFunExtFor`

This PR eliminates super-linear kernel type checking overhead when
simplifying lambda expressions. I improved the proof term produced
by `mkFunext`. This function is used in `Sym.simp` when simplifying lambda
expressions.

 ### Lambda benchmark: before vs after optimization

| Lambda | Before simp (ms) | After simp (ms) | Simp speedup | Before kernel (ms) | After kernel (ms) | Kernel speedup | Before proof | After proof | Proof reduction |
|--------|------------------|-----------------|--------------|--------------------|-------------------|----------------|--------------|-------------|-----------------|
| 10  | 0.269 | 0.208 | 1.29× | 0.521 | 0.390 | 1.34× | 583 | 498 | 1.17× |
| 20  | 0.457 | 0.382 | 1.20× | 1.126 | 0.651 | 1.73× | 1323 | 918 | 1.44× |
| 30  | 0.747 | 0.536 | 1.39× | 1.733 | 0.789 | 2.20× | 2263 | 1338 | 1.69× |
| 40  | 0.819 | 0.697 | 1.18× | 2.696 | 1.065 | 2.53× | 3403 | 1758 | 1.94× |
| 50  | 1.035 | 0.901 | 1.15× | 3.918 | 1.304 | 3.01× | 4743 | 2178 | 2.18× |
| 100 | 2.351 | 1.823 | 1.29× | 20.073 | 2.927 | 6.86× | 14443 | 4278 | 3.38× |
| 150 | 3.920 | 2.873 | 1.36× | 60.266 | 5.290 | 11.39× | 29143 | 6378 | 4.57× |
| 200 | 5.869 | 3.819 | 1.54× | 148.681 | 6.903 | 21.54× | 48843 | 8478 | 5.76× |

We can now handle much larger lambda expressions. For example:

lambda_1000: 20.869250ms, kernel: 98.637875ms, proof_size=42078

This new approach will be implemented in `Meta.simp` in the future.
Here is the table with the `Meta.simp` numbers.

 ### Old `Meta.simp` lambda benchmark

| Lambda | Simp time (ms) | Kernel time (ms) | Proof size |
|--------|----------------|------------------|------------|
| 10  | 2.308 | 0.667 | 1273 |
| 20  | 5.739 | 1.817 | 3323 |
| 30  | 10.687 | 3.320 | 6173 |
| 40  | 17.607 | 6.326 | 9823 |
| 50  | 28.336 | 9.024 | 14273 |
| 60  | 41.414 | 12.264 | 19523 |
| 70  | 59.164 | 17.388 | 25573 |
| 80  | 81.993 | 22.977 | 32423 |
| 90  | 109.785 | 27.994 | 40073 |
| 100 | 137.878 | 34.344 | 48523 |
| 110 | 173.772 | 40.477 | 57773 |
| 120 | 220.171 | 48.127 | 67823 |
| 130 | 268.921 | 56.363 | 78673 |
| 140 | 332.853 | 67.250 | 90323 |
| 150 | 395.429 | 77.329 | 102773 |
| 160 | 472.871 | 92.030 | 116023 |
| 170 | 562.862 | 102.680 | 130073 |
| 180 | 667.224 | 114.839 | 144923 |
| 190 | 761.484 | 127.277 | 160573 |
| 200 | 866.097 | 143.020 | 177023 |