Add some Proper lemmas for Option.bind

Timing diff is probably mostly noise.

After     | File Name                                                            | Before    || Change    | % Change
--------------------------------------------------------------------------------------------------------------------
68m18.12s | Total                                                                | 69m59.63s || -1m41.51s | -2.41%
--------------------------------------------------------------------------------------------------------------------
3m42.71s  | Curves/Montgomery/XZProofs.vo                                        | 4m08.00s  || -0m25.28s | -10.19%
1m22.09s  | Experiments/NewPipeline/Arithmetic.vo                                | 1m37.69s  || -0m15.59s | -15.96%
0m51.83s  | Demo.vo                                                              | 1m04.94s  || -0m13.10s | -20.18%
8m50.46s  | Experiments/SimplyTypedArithmetic.vo                                 | 8m59.22s  || -0m08.75s | -1.62%
0m36.08s  | Experiments/NewPipeline/LanguageInversion.vo                         | 0m40.70s  || -0m04.62s | -11.35%
0m27.04s  | Primitives/EdDSARepChange.vo                                         | 0m31.77s  || -0m04.73s | -14.88%
0m12.16s  | Primitives/MxDHRepChange.vo                                          | 0m16.64s  || -0m04.48s | -26.92%
4m08.54s  | Experiments/NewPipeline/RewriterRulesGood.vo                         | 4m11.60s  || -0m03.06s | -1.21%
0m36.33s  | Spec/Ed25519.vo                                                      | 0m39.60s  || -0m03.27s | -8.25%
0m19.06s  | Curves/Edwards/XYZT/Basic.vo                                         | 0m22.22s  || -0m03.16s | -14.22%
0m16.06s  | Curves/Edwards/AffineProofs.vo                                       | 0m19.36s  || -0m03.30s | -17.04%
4m44.06s  | Experiments/NewPipeline/Toplevel1.vo                                 | 4m42.03s  || +0m02.03s | +0.71%
0m08.29s  | Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.vo          | 0m10.95s  || -0m02.66s | -24.29%
6m03.41s  | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo                | 6m04.65s  || -0m01.23s | -0.34%
1m21.61s  | Compilers/Named/MapCastInterp.vo                                     | 1m22.75s  || -0m01.14s | -1.37%
1m20.35s  | Specific/X2448/Karatsuba/C64/femul.vo                                | 1m18.81s  || +0m01.53s | +1.95%
1m17.46s  | Experiments/NewPipeline/Rewriter.vo                                  | 1m18.83s  || -0m01.36s | -1.73%
0m49.98s  | Compilers/Z/Named/RewriteAddToAdcInterp.vo                           | 0m51.46s  || -0m01.48s | -2.87%
0m40.08s  | Experiments/NewPipeline/AbstractInterpretationWf.vo                  | 0m41.56s  || -0m01.48s | -3.56%
0m18.14s  | Specific/X25519/C64/fesquare.vo                                      | 0m17.02s  || +0m01.12s | +6.58%
0m14.21s  | Specific/X25519/C64/fesub.vo                                         | 0m13.13s  || +0m01.08s | +8.22%
2m09.85s  | Specific/X25519/C64/ladderstep.vo                                    | 2m09.46s  || +0m00.38s | +0.30%
1m53.52s  | Specific/NISTP256/AMD64/femul.vo                                     | 1m52.76s  || +0m00.76s | +0.67%
1m43.25s  | Experiments/NewPipeline/Toplevel2.vo                                 | 1m43.48s  || -0m00.22s | -0.22%
1m23.40s  | Experiments/NewPipeline/RewriterWf2.vo                               | 1m23.42s  || -0m00.01s | -0.02%
1m00.91s  | Specific/X25519/C32/femul.vo                                         | 1m00.02s  || +0m00.88s | +1.48%
0m50.13s  | Compilers/Z/ArithmeticSimplifierInterp.vo                            | 0m50.62s  || -0m00.48s | -0.96%
0m44.22s  | Specific/X25519/C32/fesquare.vo                                      | 0m43.65s  || +0m00.57s | +1.30%
0m41.83s  | Arithmetic/Karatsuba.vo                                              | 0m42.24s  || -0m00.41s | -0.97%
0m36.88s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery      | 0m37.49s  || -0m00.60s | -1.62%
0m34.72s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery    | 0m35.07s  || -0m00.35s | -0.99%
0m34.10s  | Specific/X25519/C32/freeze.vo                                        | 0m33.90s  || +0m00.20s | +0.58%
0m31.88s  | Compilers/Z/ArithmeticSimplifierWf.vo                                | 0m32.83s  || -0m00.94s | -2.89%
0m29.11s  | Compilers/CommonSubexpressionEliminationWf.vo                        | 0m29.30s  || -0m00.19s | -0.64%
0m27.43s  | Specific/NISTP256/AMD128/femul.vo                                    | 0m27.71s  || -0m00.28s | -1.01%
0m26.28s  | Experiments/NewPipeline/UnderLetsProofs.vo                           | 0m26.40s  || -0m00.11s | -0.45%
0m25.69s  | Specific/X25519/C32/fecarry.vo                                       | 0m25.42s  || +0m00.26s | +1.06%
0m23.18s  | Experiments/NewPipeline/AbstractInterpretationZRangeProofs.vo        | 0m23.52s  || -0m00.33s | -1.44%
0m22.69s  | Experiments/NewPipeline/LanguageWf.vo                                | 0m23.42s  || -0m00.73s | -3.11%
0m21.49s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas        | 0m20.67s  || +0m00.81s | +3.96%
0m21.40s  | Specific/X25519/C32/fesub.vo                                         | 0m21.31s  || +0m00.08s | +0.42%
0m21.31s  | Arithmetic/Core.vo                                                   | 0m21.44s  || -0m00.13s | -0.60%
0m21.06s  | Specific/X25519/C64/femul.vo                                         | 0m20.44s  || +0m00.61s | +3.03%
0m20.85s  | Specific/NISTP256/AMD64/fesub.vo                                     | 0m20.95s  || -0m00.09s | -0.47%
0m19.43s  | Specific/X25519/C32/Synthesis.vo                                     | 0m19.62s  || -0m00.19s | -0.96%
0m19.30s  | Specific/X25519/C32/feadd.vo                                         | 0m19.32s  || -0m00.01s | -0.10%
0m19.04s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas          | 0m18.91s  || +0m00.12s | +0.68%
0m19.02s  | Experiments/NewPipeline/AbstractInterpretationProofs.vo              | 0m19.52s  || -0m00.50s | -2.56%
0m18.98s  | Specific/NISTP256/AMD64/feadd.vo                                     | 0m19.82s  || -0m00.83s | -4.23%
0m18.04s  | Compilers/Named/MapCastWf.vo                                         | 0m18.28s  || -0m00.24s | -1.31%
0m18.02s  | Compilers/Z/CNotations.vo                                            | 0m18.45s  || -0m00.42s | -2.33%
0m17.41s  | Specific/X25519/C64/freeze.vo                                        | 0m17.68s  || -0m00.26s | -1.52%
0m16.00s  | Specific/NISTP256/AMD64/feopp.vo                                     | 0m15.60s  || +0m00.40s | +2.56%
0m15.61s  | Compilers/Named/ContextProperties/SmartMap.vo                        | 0m16.10s  || -0m00.49s | -3.04%
0m15.22s  | Compilers/Named/ContextProperties/NameUtil.vo                        | 0m15.78s  || -0m00.55s | -3.54%
0m14.91s  | Specific/NISTP256/AMD128/fesub.vo                                    | 0m15.34s  || -0m00.42s | -2.80%
0m14.78s  | Specific/NISTP256/AMD128/feadd.vo                                    | 0m14.79s  || -0m00.00s | -0.06%
0m14.41s  | Specific/NISTP256/AMD64/fenz.vo                                      | 0m14.14s  || +0m00.26s | +1.90%
0m14.35s  | Specific/X25519/C64/fecarry.vo                                       | 0m14.26s  || +0m00.08s | +0.63%
0m14.25s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas          | 0m14.13s  || +0m00.11s | +0.84%
0m13.95s  | Arithmetic/Saturated/AddSub.vo                                       | 0m14.02s  || -0m00.07s | -0.49%
0m13.59s  | Specific/NISTP256/AMD128/fenz.vo                                     | 0m13.65s  || -0m00.06s | -0.43%
0m13.15s  | Experiments/NewPipeline/CStringification.vo                          | 0m13.15s  || +0m00.00s | +0.00%
0m12.63s  | Compilers/Z/Syntax/Equality.vo                                       | 0m12.57s  || +0m00.06s | +0.47%
0m12.30s  | Util/ZRange/LandLorBounds.vo                                         | 0m12.78s  || -0m00.47s | -3.75%
0m12.18s  | Specific/X25519/C64/feadd.vo                                         | 0m11.87s  || +0m00.31s | +2.61%
0m12.15s  | Specific/NISTP256/AMD128/feopp.vo                                    | 0m12.28s  || -0m00.12s | -1.05%
0m11.74s  | Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.vo    | 0m12.46s  || -0m00.72s | -5.77%
0m11.30s  | Arithmetic/Saturated/MontgomeryAPI.vo                                | 0m11.54s  || -0m00.23s | -2.07%
0m10.82s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas            | 0m10.48s  || +0m00.33s | +3.24%
0m10.71s  | Arithmetic/Saturated/Core.vo                                         | 0m11.36s  || -0m00.64s | -5.72%
0m09.90s  | Specific/X2448/Karatsuba/C64/Synthesis.vo                            | 0m09.64s  || +0m00.25s | +2.69%
0m08.95s  | Util/ZRange/CornersMonotoneBounds.vo                                 | 0m09.41s  || -0m00.46s | -4.88%
0m08.77s  | LegacyArithmetic/Double/Proofs/Multiply.vo                           | 0m08.62s  || +0m00.15s | +1.74%
0m08.72s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml   | 0m08.95s  || -0m00.22s | -2.56%
0m08.66s  | LegacyArithmetic/ArchitectureToZLikeProofs.vo                        | 0m08.49s  || +0m00.16s | +2.00%
0m08.53s  | LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.vo      | 0m08.51s  || +0m00.01s | +0.23%
0m08.40s  | Compilers/Named/CompileInterpSideConditions.vo                       | 0m07.55s  || +0m00.85s | +11.25%
0m08.12s  | Compilers/Named/RegisterAssignInterp.vo                              | 0m08.36s  || -0m00.24s | -2.87%
0m07.55s  | Compilers/InlineConstAndOpWf.vo                                      | 0m07.59s  || -0m00.04s | -0.52%
0m07.06s  | Specific/NISTP256/AMD64/Synthesis.vo                                 | 0m06.96s  || +0m00.09s | +1.43%
0m06.47s  | Arithmetic/Saturated/MulSplit.vo                                     | 0m06.55s  || -0m00.08s | -1.22%
0m06.24s  | Compilers/InlineWf.vo                                                | 0m06.17s  || +0m00.07s | +1.13%
0m06.14s  | Compilers/Z/Bounds/InterpretationLemmas/PullCast.vo                  | 0m06.34s  || -0m00.20s | -3.15%
0m05.93s  | Specific/X25519/C64/Synthesis.vo                                     | 0m05.89s  || +0m00.04s | +0.67%
0m05.81s  | Compilers/LinearizeWf.vo                                             | 0m05.69s  || +0m00.11s | +2.10%
0m05.54s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.33s  || +0m00.20s | +3.93%
0m05.54s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml       | 0m05.62s  || -0m00.08s | -1.42%
0m05.48s  | Compilers/Z/HexNotationConstants.vo                                  | 0m05.47s  || +0m00.01s | +0.18%
0m05.14s  | Compilers/WfProofs.vo                                                | 0m05.06s  || +0m00.08s | +1.58%
0m05.06s  | LegacyArithmetic/Double/Proofs/RippleCarryAddSub.vo                  | 0m05.51s  || -0m00.45s | -8.16%
0m04.78s  | LegacyArithmetic/Double/Proofs/SpreadLeftImmediate.vo                | 0m04.97s  || -0m00.18s | -3.82%
0m04.74s  | Experiments/NewPipeline/RewriterWf1.vo                               | 0m04.78s  || -0m00.04s | -0.83%
0m04.46s  | Compilers/Z/BinaryNotationConstants.vo                               | 0m04.52s  || -0m00.05s | -1.32%
0m04.38s  | Compilers/Z/Bounds/Pipeline/Definition.vo                            | 0m04.56s  || -0m00.17s | -3.94%
0m04.34s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs     | 0m04.03s  || +0m00.30s | +7.69%
0m04.28s  | Compilers/Named/CompileWf.vo                                         | 0m04.21s  || +0m00.07s | +1.66%
0m04.13s  | Specific/Framework/ArithmeticSynthesis/Montgomery.vo                 | 0m04.05s  || +0m00.08s | +1.97%
0m04.01s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml         | 0m04.04s  || -0m00.03s | -0.74%
0m04.00s  | Experiments/NewPipeline/MiscCompilerPassesProofs.vo                  | 0m03.92s  || +0m00.08s | +2.04%
0m03.92s  | Arithmetic/MontgomeryReduction/WordByWord/Proofs.vo                  | 0m03.88s  || +0m00.04s | +1.03%
0m03.68s  | Compilers/EtaWf.vo                                                   | 0m04.40s  || -0m00.72s | -16.36%
0m03.47s  | Compilers/Z/ArithmeticSimplifier.vo                                  | 0m03.52s  || -0m00.04s | -1.42%
0m03.36s  | Specific/NISTP256/AMD128/Synthesis.vo                                | 0m03.25s  || +0m00.10s | +3.38%
0m03.28s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs       | 0m03.18s  || +0m00.09s | +3.14%
0m03.06s  | Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.vo               | 0m03.02s  || +0m00.04s | +1.32%
0m03.05s  | Compilers/InlineInterp.vo                                            | 0m02.95s  || +0m00.09s | +3.38%
0m03.01s  | LegacyArithmetic/Double/Proofs/ShiftRight.vo                         | 0m02.98s  || +0m00.02s | +1.00%
0m02.97s  | Compilers/Named/ContextProperties.vo                                 | 0m02.94s  || +0m00.03s | +1.02%
0m02.96s  | LegacyArithmetic/Double/Proofs/ShiftLeft.vo                          | 0m02.84s  || +0m00.12s | +4.22%
0m02.86s  | Compilers/Named/CompileInterp.vo                                     | 0m02.76s  || +0m00.10s | +3.62%
0m02.66s  | Compilers/TestCase.vo                                                | 0m02.56s  || +0m00.10s | +3.90%
0m02.61s  | Arithmetic/Saturated/Freeze.vo                                       | 0m02.52s  || +0m00.08s | +3.57%
0m02.54s  | Compilers/Named/ContextProperties/Proper.vo                          | 0m02.60s  || -0m00.06s | -2.30%
0m02.52s  | LegacyArithmetic/InterfaceProofs.vo                                  | 0m02.96s  || -0m00.43s | -14.86%
0m02.37s  | LegacyArithmetic/Double/Proofs/Decode.vo                             | 0m02.42s  || -0m00.04s | -2.06%
0m02.36s  | Compilers/CommonSubexpressionEliminationProperties.vo                | 0m02.42s  || -0m00.06s | -2.47%
0m02.36s  | Specific/NISTP256/FancyMachine256/Montgomery.vo                      | 0m02.32s  || +0m00.04s | +1.72%
0m02.26s  | Specific/NISTP256/FancyMachine256/Barrett.vo                         | 0m02.26s  || +0m00.00s | +0.00%
0m02.17s  | Compilers/Z/RewriteAddToAdcInterp.vo                                 | 0m02.15s  || +0m00.02s | +0.93%
0m02.15s  | Compilers/Z/Bounds/Relax.vo                                          | 0m02.23s  || -0m00.08s | -3.58%
0m02.10s  | Specific/Framework/ArithmeticSynthesis/Defaults.vo                   | 0m02.09s  || +0m00.01s | +0.47%
0m02.09s  | Compilers/Named/NameUtilProperties.vo                                | 0m02.05s  || +0m00.04s | +1.95%
0m01.94s  | Specific/NISTP256/FancyMachine256/Core.vo                            | 0m02.00s  || -0m00.06s | -3.00%
0m01.93s  | Compilers/WfReflective.vo                                            | 0m01.94s  || -0m00.01s | -0.51%
0m01.89s  | Compilers/Z/JavaNotations.vo                                         | 0m02.15s  || -0m00.26s | -12.09%
0m01.73s  | Arithmetic/CoreUnfolder.vo                                           | 0m01.62s  || +0m00.10s | +6.79%
0m01.66s  | Util/Tuple.vo                                                        | 0m02.11s  || -0m00.44s | -21.32%
0m01.62s  | Compilers/Named/WfFromUnit.vo                                        | 0m01.64s  || -0m00.01s | -1.21%
0m01.58s  | Compilers/Relations.vo                                               | 0m01.48s  || +0m00.10s | +6.75%
0m01.51s  | Compilers/Named/InterpretToPHOASWf.vo                                | 0m01.48s  || +0m00.03s | +2.02%
0m01.50s  | Specific/Framework/OutputType.vo                                     | 0m01.50s  || +0m00.00s | +0.00%
0m01.46s  | Experiments/NewPipeline/CLI.vo                                       | 0m01.46s  || +0m00.00s | +0.00%
0m01.36s  | Util/ZRange/SplitBounds.vo                                           | 0m01.36s  || +0m00.00s | +0.00%
0m01.32s  | Specific/Framework/ArithmeticSynthesis/Karatsuba.vo                  | 0m01.36s  || -0m00.04s | -2.94%
0m01.28s  | Curves/Edwards/XYZT/Precomputed.vo                                   | 0m01.28s  || +0m00.00s | +0.00%
0m01.28s  | Experiments/NewPipeline/Language.vo                                  | 0m01.49s  || -0m00.20s | -14.09%
0m01.27s  | Experiments/NewPipeline/StandaloneHaskellMain.vo                     | 0m01.29s  || -0m00.02s | -1.55%
0m01.26s  | Experiments/NewPipeline/StandaloneOCamlMain.vo                       | 0m01.28s  || -0m00.02s | -1.56%
0m01.22s  | Specific/Framework/ArithmeticSynthesis/Base.vo                       | 0m01.32s  || -0m00.10s | -7.57%
0m01.20s  | Compilers/LinearizeInterp.vo                                         | 0m01.20s  || +0m00.00s | +0.00%
0m01.15s  | Experiments/NewPipeline/CompilersTestCases.vo                        | 0m01.04s  || +0m00.10s | +10.57%
0m01.11s  | Compilers/MultiSizeTest.vo                                           | 0m01.14s  || -0m00.02s | -2.63%
0m01.08s  | Arithmetic/Saturated/CoreUnfolder.vo                                 | 0m01.10s  || -0m00.02s | -1.81%
0m01.06s  | Compilers/Z/RewriteAddToAdcWf.vo                                     | 0m01.13s  || -0m00.06s | -6.19%
0m01.06s  | LegacyArithmetic/Double/Proofs/BitwiseOr.vo                          | 0m01.10s  || -0m00.04s | -3.63%
0m01.04s  | Experiments/NewPipeline/AbstractInterpretation.vo                    | 0m01.05s  || -0m00.01s | -0.95%
0m01.04s  | Util/ZRange/BasicLemmas.vo                                           | 0m01.04s  || +0m00.00s | +0.00%
0m00.98s  | Arithmetic/Saturated/WrappersUnfolder.vo                             | 0m01.03s  || -0m00.05s | -4.85%
0m00.97s  | Specific/Framework/IntegrationTestDisplayCommon.vo                   | 0m00.91s  || +0m00.05s | +6.59%
0m00.97s  | Specific/X25519/C32/CurveParameters.vo                               | 0m00.99s  || -0m00.02s | -2.02%
0m00.96s  | Compilers/Named/InterpretToPHOASInterp.vo                            | 0m01.00s  || -0m00.04s | -4.00%
0m00.96s  | Specific/Framework/SynthesisFramework.vo                             | 0m00.96s  || +0m00.00s | +0.00%
0m00.95s  | Experiments/NewPipeline/RewriterProofs.vo                            | 0m00.88s  || +0m00.06s | +7.95%
0m00.93s  | Compilers/Z/Bounds/Pipeline/ReflectiveTactics.vo                     | 0m00.87s  || +0m00.06s | +6.89%
0m00.92s  | Specific/Framework/ReificationTypes.vo                               | 0m00.95s  || -0m00.02s | -3.15%
0m00.90s  | Compilers/InterpByIsoProofs.vo                                       | 0m00.81s  || +0m00.08s | +11.11%
0m00.89s  | Compilers/Named/CompileProperties.vo                                 | 0m00.84s  || +0m00.05s | +5.95%
0m00.88s  | Compilers/Named/InterpSideConditionsInterp.vo                        | 0m00.80s  || +0m00.07s | +9.99%
0m00.88s  | Specific/Framework/ArithmeticSynthesis/Freeze.vo                     | 0m00.89s  || -0m00.01s | -1.12%
0m00.86s  | Compilers/Z/CommonSubexpressionElimination.vo                        | 0m00.89s  || -0m00.03s | -3.37%
0m00.85s  | LegacyArithmetic/Double/Proofs/LoadImmediate.vo                      | 0m00.86s  || -0m00.01s | -1.16%
0m00.84s  | Compilers/Z/Syntax/Util.vo                                           | 0m00.86s  || -0m00.02s | -2.32%
0m00.83s  | Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.vo          | 0m00.74s  || +0m00.08s | +12.16%
0m00.83s  | Specific/Framework/ArithmeticSynthesis/SquareFromMul.vo              | 0m00.73s  || +0m00.09s | +13.69%
0m00.82s  | Arithmetic/Saturated/UniformWeight.vo                                | 0m00.83s  || -0m00.01s | -1.20%
0m00.82s  | Specific/Framework/MontgomeryReificationTypes.vo                     | 0m00.74s  || +0m00.07s | +10.81%
0m00.81s  | Compilers/Named/FMapContext.vo                                       | 0m00.85s  || -0m00.03s | -4.70%
0m00.81s  | Compilers/WfInversion.vo                                             | 0m01.00s  || -0m00.18s | -18.99%
0m00.80s  | Specific/Framework/IntegrationTestTemporaryMiscCommon.vo             | 0m00.85s  || -0m00.04s | -5.88%
0m00.79s  | Arithmetic/Saturated/MulSplitUnfolder.vo                             | 0m00.90s  || -0m00.10s | -12.22%
0m00.78s  | Arithmetic/Saturated/FreezeUnfolder.vo                               | 0m00.78s  || +0m00.00s | +0.00%
0m00.78s  | LegacyArithmetic/Double/Proofs/SelectConditional.vo                  | 0m00.70s  || +0m00.08s | +11.42%
0m00.78s  | Specific/Framework/ArithmeticSynthesis/BasePackage.vo                | 0m00.69s  || +0m00.09s | +13.04%
0m00.77s  | Specific/Framework/MontgomeryReificationTypesPackage.vo              | 0m00.76s  || +0m00.01s | +1.31%
0m00.76s  | Compilers/Named/AListContext.vo                                      | 0m00.82s  || -0m00.05s | -7.31%
0m00.75s  | Specific/Framework/ArithmeticSynthesis/DefaultsPackage.vo            | 0m00.70s  || +0m00.05s | +7.14%
0m00.74s  | Arithmetic/MontgomeryReduction/WordByWord/Definition.vo              | 0m00.72s  || +0m00.02s | +2.77%
0m00.74s  | Specific/Framework/ArithmeticSynthesis/FreezePackage.vo              | 0m00.78s  || -0m00.04s | -5.12%
0m00.74s  | Specific/Framework/ArithmeticSynthesis/Ladderstep.vo                 | 0m00.71s  || +0m00.03s | +4.22%
0m00.74s  | Specific/Framework/ReificationTypesPackage.vo                        | 0m00.73s  || +0m00.01s | +1.36%
0m00.73s  | Compilers/MapCastByDeBruijnInterp.vo                                 | 0m00.75s  || -0m00.02s | -2.66%
0m00.73s  | Specific/Framework/ArithmeticSynthesis/LadderstepPackage.vo          | 0m00.71s  || +0m00.02s | +2.81%
0m00.72s  | Arithmetic/Saturated/UniformWeightInstances.vo                       | 0m00.64s  || +0m00.07s | +12.49%
0m00.72s  | Compilers/InlineConstAndOpInterp.vo                                  | 0m00.78s  || -0m00.06s | -7.69%
0m00.71s  | Specific/Framework/ArithmeticSynthesis/HelperTactics.vo              | 0m00.69s  || +0m00.02s | +2.89%
0m00.71s  | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage.vo           | 0m00.70s  || +0m00.01s | +1.42%
0m00.70s  | Util/CPSUtil.vo                                                      | 0m00.86s  || -0m00.16s | -18.60%
0m00.69s  | Compilers/SmartMap.vo                                                | 0m00.72s  || -0m00.03s | -4.16%
0m00.69s  | Experiments/NewPipeline/MiscCompilerPasses.vo                        | 0m01.00s  || -0m00.31s | -31.00%
0m00.67s  | Arithmetic/Saturated/Wrappers.vo                                     | 0m00.66s  || +0m00.01s | +1.51%
0m00.66s  | Compilers/CommonSubexpressionEliminationInterp.vo                    | 0m00.69s  || -0m00.02s | -4.34%
0m00.65s  | Compilers/CommonSubexpressionElimination.vo                          | 0m00.64s  || +0m00.01s | +1.56%
0m00.63s  | LegacyArithmetic/Interface.vo                                        | 0m00.87s  || -0m00.24s | -27.58%
0m00.62s  | Compilers/WfReflectiveGen.vo                                         | 0m00.66s  || -0m00.04s | -6.06%
0m00.61s  | Compilers/Z/Bounds/MapCastByDeBruijnInterp.vo                        | 0m00.62s  || -0m00.01s | -1.61%
0m00.61s  | Compilers/Z/Bounds/Pipeline.vo                                       | 0m00.72s  || -0m00.10s | -15.27%
0m00.60s  | Compilers/MapCastByDeBruijnWf.vo                                     | 0m00.61s  || -0m00.01s | -1.63%
0m00.59s  | Compilers/Named/WfInterp.vo                                          | 0m00.57s  || +0m00.02s | +3.50%
0m00.58s  | Compilers/InlineConstAndOpByRewriteWf.vo                             | 0m00.54s  || +0m00.03s | +7.40%
0m00.58s  | Compilers/MapBaseTypeWf.vo                                           | 0m00.63s  || -0m00.05s | -7.93%
0m00.58s  | Compilers/Z/Named/RewriteAddToAdc.vo                                 | 0m00.64s  || -0m00.06s | -9.37%
0m00.57s  | Compilers/Z/MapCastByDeBruijnInterp.vo                               | 0m00.51s  || +0m00.05s | +11.76%
0m00.57s  | Compilers/Z/Syntax.vo                                                | 0m00.61s  || -0m00.04s | -6.55%
0m00.57s  | Experiments/PartialEvaluationWithLetIn.vo                            | 0m00.57s  || +0m00.00s | +0.00%
0m00.56s  | Compilers/Z/Bounds/InterpretationLemmas/Tactics.vo                   | 0m00.55s  || +0m00.01s | +1.81%
0m00.56s  | Compilers/Z/Bounds/Pipeline/Glue.vo                                  | 0m00.55s  || +0m00.01s | +1.81%
0m00.55s  | Compilers/Z/Reify.vo                                                 | 0m00.53s  || +0m00.02s | +3.77%
0m00.54s  | Compilers/InterpWfRel.vo                                             | 0m00.54s  || +0m00.00s | +0.00%
0m00.54s  | Compilers/Z/Bounds/RoundUpLemmas.vo                                  | 0m00.56s  || -0m00.02s | -3.57%
0m00.54s  | LegacyArithmetic/Double/Core.vo                                      | 0m00.52s  || +0m00.02s | +3.84%
0m00.54s  | LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic.vo               | 0m00.49s  || +0m00.05s | +10.20%
0m00.54s  | Util/Decidable/Decidable2Bool.vo                                     | 0m00.69s  || -0m00.14s | -21.73%
0m00.53s  | Compilers/Z/CommonSubexpressionEliminationInterp.vo                  | 0m00.49s  || +0m00.04s | +8.16%
0m00.52s  | Compilers/ExprInversion.vo                                           | 0m00.44s  || +0m00.08s | +18.18%
0m00.52s  | Compilers/GeneralizeVarInterp.vo                                     | 0m00.51s  || +0m00.01s | +1.96%
0m00.52s  | Compilers/InterpWf.vo                                                | 0m00.49s  || +0m00.03s | +6.12%
0m00.52s  | Compilers/Z/InlineConstAndOp.vo                                      | 0m00.40s  || +0m00.12s | +30.00%
0m00.52s  | Compilers/Z/RewriteAddToAdc.vo                                       | 0m00.51s  || +0m00.01s | +1.96%
0m00.52s  | Util/HList.vo                                                        | 0m00.59s  || -0m00.06s | -11.86%
0m00.51s  | Compilers/InputSyntax.vo                                             | 0m00.52s  || -0m00.01s | -1.92%
0m00.51s  | Compilers/Z/Bounds/MapCastByDeBruijnWf.vo                            | 0m00.58s  || -0m00.06s | -12.06%
0m00.51s  | Compilers/Z/CommonSubexpressionEliminationWf.vo                      | 0m00.51s  || +0m00.00s | +0.00%
0m00.50s  | Compilers/Z/Bounds/MapCastByDeBruijn.vo                              | 0m00.53s  || -0m00.03s | -5.66%
0m00.50s  | Compilers/Z/FoldTypes.vo                                             | 0m00.49s  || +0m00.01s | +2.04%
0m00.50s  | Util/ZBounded.vo                                                     | 0m00.54s  || -0m00.04s | -7.40%
0m00.49s  | Compilers/Z/MapCastByDeBruijn.vo                                     | 0m00.48s  || +0m00.01s | +2.08%
0m00.49s  | Experiments/NewPipeline/UnderLets.vo                                 | 0m00.55s  || -0m00.06s | -10.90%
0m00.47s  | Compilers/GeneralizeVarWf.vo                                         | 0m00.46s  || +0m00.00s | +2.17%
0m00.47s  | Compilers/Named/PositiveContext/DefaultsProperties.vo                | 0m00.51s  || -0m00.04s | -7.84%
0m00.47s  | Compilers/Z/MapCastByDeBruijnWf.vo                                   | 0m00.47s  || +0m00.00s | +0.00%
0m00.47s  | LegacyArithmetic/ArchitectureToZLike.vo                              | 0m00.49s  || -0m00.02s | -4.08%
0m00.47s  | Util/AdditionChainExponentiation.vo                                  | 0m00.44s  || +0m00.02s | +6.81%
0m00.46s  | Compilers/Named/DeadCodeEliminationInterp.vo                         | 0m00.49s  || -0m00.02s | -6.12%
0m00.46s  | Compilers/Named/WeakListContext.vo                                   | 0m00.42s  || +0m00.04s | +9.52%
0m00.46s  | Compilers/Z/Bounds/Interpretation.vo                                 | 0m00.45s  || +0m00.01s | +2.22%
0m00.46s  | Compilers/Z/GeneralizeVarInterp.vo                                   | 0m00.49s  || -0m00.02s | -6.12%
0m00.46s  | Compilers/Z/InlineConstAndOpByRewrite.vo                             | 0m00.44s  || +0m00.02s | +4.54%
0m00.46s  | Compilers/Z/InlineConstAndOpInterp.vo                                | 0m00.50s  || -0m00.03s | -7.99%
0m00.46s  | Compilers/Z/InlineWf.vo                                              | 0m00.45s  || +0m00.01s | +2.22%
0m00.46s  | Compilers/Z/InterpSideConditions.vo                                  | 0m00.50s  || -0m00.03s | -7.99%
0m00.46s  | Compilers/Z/Named/DeadCodeElimination.vo                             | 0m00.39s  || +0m00.07s | +17.94%
0m00.46s  | Specific/Framework/CurveParameters.vo                                | 0m00.46s  || +0m00.00s | +0.00%
0m00.46s  | Specific/X25519/C64/CurveParameters.vo                               | 0m00.49s  || -0m00.02s | -6.12%
0m00.45s  | Compilers/Z/ArithmeticSimplifierUtil.vo                              | 0m00.48s  || -0m00.02s | -6.24%
0m00.45s  | Compilers/Z/GeneralizeVarWf.vo                                       | 0m00.42s  || +0m00.03s | +7.14%
0m00.45s  | Compilers/Z/Inline.vo                                                | 0m00.47s  || -0m00.01s | -4.25%
0m00.45s  | Compilers/Z/InlineInterp.vo                                          | 0m00.47s  || -0m00.01s | -4.25%
0m00.44s  | Compilers/InlineConstAndOpByRewriteInterp.vo                         | 0m00.43s  || +0m00.01s | +2.32%
0m00.44s  | Compilers/Z/InlineConstAndOpByRewriteWf.vo                           | 0m00.51s  || -0m00.07s | -13.72%
0m00.44s  | Compilers/Z/InlineConstAndOpWf.vo                                    | 0m00.52s  || -0m00.08s | -15.38%
0m00.44s  | Compilers/ZExtended/Syntax.vo                                        | 0m00.59s  || -0m00.14s | -25.42%
0m00.44s  | Specific/Framework/IntegrationTestDisplayCommonTactics.vo            | 0m00.43s  || +0m00.01s | +2.32%
0m00.43s  | Compilers/ZExtended/MapBaseType.vo                                   | 0m00.48s  || -0m00.04s | -10.41%
0m00.42s  | Compilers/InlineConstAndOp.vo                                        | 0m00.46s  || -0m00.04s | -8.69%
0m00.42s  | Compilers/InterpProofs.vo                                            | 0m00.44s  || -0m00.02s | -4.54%
0m00.42s  | Compilers/Named/PositiveContext/Defaults.vo                          | 0m00.36s  || +0m00.06s | +16.66%
0m00.42s  | Compilers/Reify.vo                                                   | 0m00.49s  || -0m00.07s | -14.28%
0m00.42s  | Compilers/Z/InlineConstAndOpByRewriteInterp.vo                       | 0m00.43s  || -0m00.01s | -2.32%
0m00.42s  | Util/ZRange.vo                                                       | 0m00.61s  || -0m00.19s | -31.14%
0m00.42s  | Util/ZRange/Operations.vo                                            | 0m00.50s  || -0m00.08s | -16.00%
0m00.41s  | Compilers/Inline.vo                                                  | 0m00.37s  || +0m00.03s | +10.81%
0m00.41s  | Compilers/Named/RegisterAssign.vo                                    | 0m00.38s  || +0m00.02s | +7.89%
0m00.41s  | Compilers/Z/Named/DeadCodeEliminationInterp.vo                       | 0m00.47s  || -0m00.06s | -12.76%
0m00.40s  | Compilers/Z/GeneralizeVar.vo                                         | 0m00.48s  || -0m00.07s | -16.66%
0m00.40s  | Specific/Framework/RawCurveParameters.vo                             | 0m00.43s  || -0m00.02s | -6.97%
0m00.40s  | Util/ZRange/Show.vo                                                  | 0m00.37s  || +0m00.03s | +8.10%
0m00.39s  | Compilers/ZExtended/InlineConstAndOpInterp.vo                        | 0m00.38s  || +0m00.01s | +2.63%
0m00.38s  | Compilers/Named/ContextProperties/Tactics.vo                         | 0m00.32s  || +0m00.06s | +18.75%
0m00.38s  | Compilers/Named/DeadCodeElimination.vo                               | 0m00.44s  || -0m00.06s | -13.63%
0m00.38s  | Compilers/Z/Bounds/Pipeline/OutputType.vo                            | 0m00.32s  || +0m00.06s | +18.75%
0m00.37s  | Compilers/CommonSubexpressionEliminationDenote.vo                    | 0m00.36s  || +0m00.01s | +2.77%
0m00.37s  | Compilers/GeneralizeVar.vo                                           | 0m00.36s  || +0m00.01s | +2.77%
0m00.37s  | Specific/X2448/Karatsuba/C64/CurveParameters.vo                      | 0m00.38s  || -0m00.01s | -2.63%
0m00.36s  | Compilers/FoldTypes.vo                                               | 0m00.34s  || +0m00.01s | +5.88%
0m00.36s  | Compilers/MapBaseType.vo                                             | 0m00.32s  || +0m00.03s | +12.49%
0m00.36s  | Compilers/MapCastByDeBruijn.vo                                       | 0m00.35s  || +0m00.01s | +2.85%
0m00.36s  | Compilers/Named/MapCast.vo                                           | 0m00.38s  || -0m00.02s | -5.26%
0m00.36s  | Compilers/Z/TypeInversion.vo                                         | 0m00.32s  || +0m00.03s | +12.49%
0m00.36s  | Compilers/ZExtended/InlineConstAndOpByRewrite.vo                     | 0m00.32s  || +0m00.03s | +12.49%
0m00.36s  | Specific/Framework/CurveParametersPackage.vo                         | 0m00.34s  || +0m00.01s | +5.88%
0m00.36s  | Specific/NISTP256/AMD128/CurveParameters.vo                          | 0m00.36s  || +0m00.00s | +0.00%
0m00.36s  | Specific/NISTP256/AMD64/CurveParameters.vo                           | 0m00.44s  || -0m00.08s | -18.18%
0m00.35s  | Compilers/CountLets.vo                                               | 0m00.32s  || +0m00.02s | +9.37%
0m00.35s  | Util/BoundedWord.vo                                                  | 0m00.60s  || -0m00.25s | -41.66%
0m00.34s  | Compilers/InlineConstAndOpByRewrite.vo                               | 0m00.34s  || +0m00.00s | +0.00%
0m00.34s  | Compilers/InterpByIso.vo                                             | 0m00.36s  || -0m00.01s | -5.55%
0m00.34s  | Compilers/Linearize.vo                                               | 0m00.34s  || +0m00.00s | +0.00%
0m00.34s  | Compilers/Named/ContextOn.vo                                         | 0m00.32s  || +0m00.02s | +6.25%
0m00.34s  | Compilers/Named/InterpSideConditions.vo                              | 0m00.35s  || -0m00.00s | -2.85%
0m00.34s  | Compilers/Named/InterpretToPHOAS.vo                                  | 0m00.30s  || +0m00.04s | +13.33%
0m00.34s  | Compilers/StripExpr.vo                                               | 0m00.31s  || +0m00.03s | +9.67%
0m00.34s  | Compilers/Z/OpInversion.vo                                           | 0m00.32s  || +0m00.02s | +6.25%
0m00.34s  | Compilers/ZExtended/Syntax/Util.vo                                   | 0m00.38s  || -0m00.03s | -10.52%
0m00.34s  | Util/IdfunWithAlt.vo                                                 | 0m00.50s  || -0m00.15s | -31.99%
0m00.33s  | Compilers/FilterLive.vo                                              | 0m00.32s  || +0m00.01s | +3.12%
0m00.33s  | Compilers/Named/Compile.vo                                           | 0m00.34s  || -0m00.01s | -2.94%
0m00.33s  | Compilers/Named/ContextDefinitions.vo                                | 0m00.34s  || -0m00.01s | -2.94%
0m00.33s  | Compilers/Named/IdContext.vo                                         | 0m00.33s  || +0m00.00s | +0.00%
0m00.33s  | Compilers/Named/PositiveContext.vo                                   | 0m00.38s  || -0m00.04s | -13.15%
0m00.32s  | Compilers/Named/CountLets.vo                                         | 0m00.32s  || +0m00.00s | +0.00%
0m00.32s  | Compilers/Named/EstablishLiveness.vo                                 | 0m00.36s  || -0m00.03s | -11.11%
0m00.32s  | Compilers/Named/GetNames.vo                                          | 0m00.30s  || +0m00.02s | +6.66%
0m00.32s  | Compilers/Named/MapType.vo                                           | 0m00.32s  || +0m00.00s | +0.00%
0m00.32s  | Compilers/Named/Syntax.vo                                            | 0m00.39s  || -0m00.07s | -17.94%
0m00.32s  | Compilers/Tuple.vo                                                   | 0m00.41s  || -0m00.08s | -21.95%
0m00.32s  | Compilers/ZExtended/InlineConstAndOpByRewriteInterp.vo               | 0m00.36s  || -0m00.03s | -11.11%
0m00.32s  | Compilers/ZExtended/InlineConstAndOpByRewriteWf.vo                   | 0m00.40s  || -0m00.08s | -20.00%
0m00.32s  | Compilers/ZExtended/InlineConstAndOpWf.vo                            | 0m00.36s  || -0m00.03s | -11.11%
0m00.31s  | Compilers/Named/ExprInversion.vo                                     | 0m00.31s  || +0m00.00s | +0.00%
0m00.31s  | Compilers/Named/Wf.vo                                                | 0m00.33s  || -0m00.02s | -6.06%
0m00.30s  | Compilers/Named/Context.vo                                           | 0m00.32s  || -0m00.02s | -6.25%
0m00.30s  | Compilers/ZExtended/InlineConstAndOp.vo                              | 0m00.34s  || -0m00.04s | -11.76%
0m00.28s  | Compilers/Named/SmartMap.vo                                          | 0m00.30s  || -0m00.01s | -6.66%
0m00.26s  | Util/SideConditions/ModInvPackage.vo                                 | 0m00.28s  || -0m00.02s | -7.14%
0m00.25s  | Util/Option.vo                                                       | 0m00.25s  || +0m00.00s | +0.00%
0m00.24s  | Util/OptionList.vo                                                   | 0m00.27s  || -0m00.03s | -11.11%
0m00.23s  | Util/SideConditions/Autosolve.vo                                     | 0m00.24s  || -0m00.00s | -4.16%
0m00.22s  | Compilers/EtaInterp.vo                                               | 0m00.29s  || -0m00.06s | -24.13%
0m00.14s  | Compilers/RewriterWf.vo                                              | 0m00.17s  || -0m00.03s | -17.64%
0m00.11s  | Util/ListUtil/SetoidList.vo                                          | 0m00.13s  || -0m00.02s | -15.38%
0m00.08s  | Compilers/InterpSideConditions.vo                                    | 0m00.07s  || +0m00.00s | +14.28%
0m00.07s  | Compilers/Eta.vo                                                     | 0m00.09s  || -0m00.01s | -22.22%
0m00.04s  | Compilers/RenameBinders.vo                                           | 0m00.08s  || -0m00.04s | -50.00%

1 files changed, 27 insertions, 0 deletions

diff --git a/src/Util/Option.v b/src/Util/Option.v
index ccbf6cff3..5d53223c2 100644
--- a/src/Util/Option.v
+++ b/src/Util/Option.v
@@ -75,6 +75,33 @@ Section Relations.
     : Equivalence (option_eq R). Proof. split; exact _. Qed.
 End Relations.
 
+Global Instance bind_Proper {A B}
+  : Proper (eq ==> (pointwise_relation _ eq) ==> eq) (@bind A B).
+Proof.
+  cbv [respectful bind pointwise_relation Proper]; intros; subst; break_innermost_match; auto.
+Qed.
+
+Global Instance bind_Proper_pointwise_option_eq {A B RB}
+  : Proper (eq ==> (pointwise_relation _ (option_eq RB)) ==> option_eq RB) (@bind A B) | 90.
+Proof.
+  cbv [respectful bind pointwise_relation Proper]; intros; subst; break_innermost_match; cbn [option_eq]; auto.
+Qed.
+
+Lemma bind_Proper_option_eq_hetero {A A' B B'} {RA RB : _ -> _ -> Prop}
+      a a' (HA : option_eq RA a a') b b' (HB : forall a a', RA a a' -> option_eq RB (b a) (b' a'))
+  : option_eq RB (@bind A B a b) (@bind A' B' a' b').
+Proof.
+  cbv [bind].
+  destruct a as [a|], a' as [a'|]; try (reflexivity || congruence || exfalso; assumption).
+  cbn [option_eq] in *; auto.
+Qed.
+
+Global Instance bind_Proper_option_eq {A B RA RB}
+  : Proper (option_eq RA ==> (RA ==> option_eq RB) ==> option_eq RB) (@bind A B) | 100.
+Proof.
+  cbv [Proper respectful]; eapply bind_Proper_option_eq_hetero.
+Qed.
+
 Global Instance Proper_option_rect_nd_changebody
       {A B:Type} {RB:relation B} {a:option A}
   : Proper (pointwise_relation _ RB ==> RB ==> RB) (fun S N => option_rect (fun _ => B) S N a).