Handle rewrite rules with binders as arguments to constructors under literals

[JasonGross]

Currently, we cannot handle rewrite rules such as

forall x, '(S x) = pred '(S (S x))

because we end up generating a pattern like forall x1 x2, x1 =? S x && x2 =? S (S x) -> 'x1 = pred 'x2, and the reification machinery does not know how to invert these equations to eliminate x: https://github.com/mit-plv/rewriter/blob/351f48c725cfc68bb698b0330722f309f8ed447d/src/Rewriter/Rewriter/Reify.v#L657-L696

Presumably we could write some sort of custom inversion machinery to handle these constructors? And/or we could emit better error messages than just

Error:
Uncaught Ltac2 exception:
RewriteRules.Reify.Cannot_eliminate_functional_dependencies
  (message:((fun u2 : Z =>
             existT
               (RewriteRules.Compile.rewrite_ruleTP
                  IdentifiersGENERATED.Compilers.pattern.ident.arg_types_unfolded)
               {|
                 pattern.type_of_anypattern :=
                   type.base
                     (pattern.base.type.type_base Compilers.Z *
                      pattern.base.type.type_base Compilers.Z)%pbtype;
                 pattern.pattern_of_anypattern :=
                   #Compilers.pattern_ident_Z_cast2 @
                   (#(Compilers.pattern_ident_pair
                        (pattern.base.type.type_base Compilers.zrange)
                        (pattern.base.type.type_base Compilers.zrange)) @
                    #(Compilers.pattern_ident_Literal Compilers.zrange) @
                    #(Compilers.pattern_ident_Literal Compilers.zrange)) @
                   (#Compilers.pattern_ident_Z_mul_split @
                    pattern.Wildcard
                      (type.base (pattern.base.type.type_base Compilers.Z)) @
                    pattern.Wildcard
                      (type.base (pattern.base.type.type_base Compilers.Z)) @
                    pattern.Wildcard
                      (type.base (pattern.base.type.type_base Compilers.Z)))
               |}
               {|
                 RewriteRules.Compile.rew_should_do_again := true;
                 RewriteRules.Compile.rew_with_opt := true;
                 RewriteRules.Compile.rew_under_lets := true;
                 RewriteRules.Compile.rew_replacement :=
                   fun (t t0 : ZRange.zrange)
                     (x0 x1
                      x2 : API.expr
                             (type.base (base.type.type_base Compilers.Z)))
                   =>
                   if
                    ((0 <=? 2 ^ bitwidth - 1)%Z && (0 <=? u1)%Z &&
                     (0 <=? u2)%Z &&
                     Definitions.Z.divideb (u1 + 1) (2 ^ bitwidth - 1 + 1) &&
                     Definitions.Z.divideb (u2 + 1) (2 ^ bitwidth - 1 + 1) &&
                     (negb (u1 =? 2 ^ bitwidth - 1)%Z
                      || negb (u2 =? 2 ^ bitwidth - 1)%Z) &&
                     ZRange.zrange_beq t
                       {| ZRange.lower := 0; ZRange.upper := u1 |} &&
                     ZRange.zrange_beq t0
                       {| ZRange.lower := 0; ZRange.upper := u2 |})%bool
                   then
                    Some
                      (RewriteRules.Reify.expr_value_to_rewrite_rule_replacement
                         (@RewriteRules.Compile.reflect_ident_iota
                            Compilers.base
                            IdentifiersBasicGENERATED.Compilers.ident
                            Compilers.base_interp Compilers.baseHasNat
                            Compilers.buildIdent Compilers.buildEagerIdent
                            Compilers.toRestrictedIdent
                            Compilers.toFromRestrictedIdent
                            Compilers.invertIdent Compilers.baseHasNatCorrect
                            Compilers.try_make_base_transport_cps var) true
                         (#Compilers.ident_Z_cast2 @
                          (###{| ZRange.lower := 0; ZRange.upper := u1 |},
                           ###{| ZRange.lower := 0; ZRange.upper := u2 |}) @
                          (#Compilers.ident_Z_cast2 @
                           (###{|
                                 ZRange.lower := 0;
                                 ZRange.upper := 2 ^ bitwidth - 1
                               |},
                            ###{|
                                 ZRange.lower := 0;
                                 ZRange.upper := 2 ^ bitwidth - 1
                               |}) @
                           (#Compilers.ident_Z_mul_split @ $$x0 @ $$x1 @ $$x2))))
                   else None
               |})))