arith_rewrite_head = 
match idc in (Compilers.ident t) return (Compile.value' true t) with
| @Literal t v => Base (##v)%expr
| Nat_succ => fun x : expr ℕ => Base (#(Nat_succ)%expr @ x)%expr_pat
| Nat_pred => fun x : expr ℕ => Base (#(Nat_pred)%expr @ x)%expr_pat
| Nat_max => fun x x0 : expr ℕ => Base (#(Nat_max)%expr @ x @ x0)%expr_pat
| Nat_mul => fun x x0 : expr ℕ => Base (#(Nat_mul)%expr @ x @ x0)%expr_pat
| Nat_add => fun x x0 : expr ℕ => Base (#(Nat_add)%expr @ x @ x0)%expr_pat
| Nat_sub => fun x x0 : expr ℕ => Base (#(Nat_sub)%expr @ x @ x0)%expr_pat
| Nat_eqb => fun x x0 : expr ℕ => Base (#(Nat_eqb)%expr @ x @ x0)%expr_pat
| @nil t => Base []%expr_pat
| @cons t => fun (x : expr t) (x0 : expr (list t)) => Base (x :: x0)%expr_pat
| @pair A B => fun (x : expr A) (x0 : expr B) => Base (x, x0)%expr_pat
| @fst A B =>
    fun x : expr (A * B)%etype =>
    ((match x with
      | @expr.App _ _ _ s _
        (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) x1) _ =>
          args <- invert_bind_args idc Raw.ident.pair;
          match
            pattern.type.unify_extracted
              ((('1 * '2)%pbtype -> '1%pbtype) ->
               (('1%pbtype -> '2%pbtype -> ('1 * '2)%pbtype) -> '1%pbtype) ->
               '2%pbtype)%ptype
              (((A * B)%etype -> A) ->
               (((let (x2, _) := args in x2) ->
                 (let (_, y) := args in y) ->
                 ((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) ->
                s0) -> s)%ptype
          with
          | Datatypes.Some (_, _, _, (_, (_, (_, _)), b3, b2))%zrange =>
              if
               type.type_beq base.type base.type.type_beq
                 (((b3 * b2)%etype -> b3) ->
                  ((b3 -> b2 -> (b3 * b2)%etype) -> b3) -> b2)%ptype
                 (((A * B)%etype -> A) ->
                  (((let (x2, _) := args in x2) ->
                    (let (_, y) := args in y) ->
                    ((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) ->
                   s0) -> s)%ptype
              then
               _ <- ident.unify pattern.ident.fst fst;
               _ <- ident.unify pattern.ident.pair pair;
               v <- type.try_make_transport_cps s0 b3;
               _ <- type.try_make_transport_cps s b2;
               v1 <- base.try_make_transport_cps b3 b3;
               _ <- base.try_make_transport_cps b2 b2;
               v3 <- base.try_make_transport_cps b3 A;
               v4 <- base.try_make_transport_cps A A;
               Datatypes.Some (Base (v4 (v3 (v1 (v (Compile.reflect x1))))))
              else Datatypes.None
          | Datatypes.None => Datatypes.None
          end
      | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App
        _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ |
        @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (_ @ _)%expr_pat _) _ |
        @expr.App _ _ _ s _
        (@expr.App _ _ _ s0 _ (@expr.LetIn _ _ _ _ _ _ _) _) _ =>
          Datatypes.None
      | @expr.App _ _ _ s _ #(_)%expr_pat _ | @expr.App _ _ _ s _ ($_)%expr
        _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s
        _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None
      | _ => Datatypes.None
      end;;
      Datatypes.None);;;
     Base (#(fst)%expr @ x)%expr_pat)%option
| @snd A B =>
    fun x : expr (A * B)%etype =>
    ((match x with
      | @expr.App _ _ _ s _
        (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) _) x0 =>
          args <- invert_bind_args idc Raw.ident.pair;
          match
            pattern.type.unify_extracted
              ((('1 * '2)%pbtype -> '2%pbtype) ->
               (('1%pbtype -> '2%pbtype -> ('1 * '2)%pbtype) -> '1%pbtype) ->
               '2%pbtype)%ptype
              (((A * B)%etype -> B) ->
               (((let (x2, _) := args in x2) ->
                 (let (_, y) := args in y) ->
                 ((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) ->
                s0) -> s)%ptype
          with
          | Datatypes.Some (_, _, _, (_, (_, (_, _)), b3, b2))%zrange =>
              if
               type.type_beq base.type base.type.type_beq
                 (((b3 * b2)%etype -> b2) ->
                  ((b3 -> b2 -> (b3 * b2)%etype) -> b3) -> b2)%ptype
                 (((A * B)%etype -> B) ->
                  (((let (x2, _) := args in x2) ->
                    (let (_, y) := args in y) ->
                    ((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) ->
                   s0) -> s)%ptype
              then
               _ <- ident.unify pattern.ident.snd snd;
               _ <- ident.unify pattern.ident.pair pair;
               _ <- type.try_make_transport_cps s0 b3;
               v0 <- type.try_make_transport_cps s b2;
               _ <- base.try_make_transport_cps b3 b3;
               v2 <- base.try_make_transport_cps b2 b2;
               v3 <- base.try_make_transport_cps b2 B;
               v4 <- base.try_make_transport_cps B B;
               Datatypes.Some (Base (v4 (v3 (v2 (v0 (Compile.reflect x0))))))
              else Datatypes.None
          | Datatypes.None => Datatypes.None
          end
      | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App
        _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ |
        @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (_ @ _)%expr_pat _) _ |
        @expr.App _ _ _ s _
        (@expr.App _ _ _ s0 _ (@expr.LetIn _ _ _ _ _ _ _) _) _ =>
          Datatypes.None
      | @expr.App _ _ _ s _ #(_)%expr_pat _ | @expr.App _ _ _ s _ ($_)%expr
        _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s
        _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None
      | _ => Datatypes.None
      end;;
      Datatypes.None);;;
     Base (#(snd)%expr @ x)%expr_pat)%option
| @prod_rect A B T =>
    fun (x : expr A -> expr B -> UnderLets (expr T))
      (x0 : expr (A * B)%etype) =>
    Base
      (#(prod_rect)%expr @
       (λ (x1 : var A)(x2 : var B),
        to_expr (x ($x1) ($x2)))%expr @ x0)%expr_pat
| @bool_rect T =>
    fun (x x0 : expr unit -> UnderLets (expr T)) (x1 : expr bool) =>
    Base
      (#(bool_rect)%expr @ (λ x2 : var unit,
                            to_expr (x ($x2)))%expr @
       (λ x2 : var unit,
        to_expr (x0 ($x2)))%expr @ x1)%expr_pat
| @nat_rect P =>
    fun (x : expr unit -> UnderLets (expr P))
      (x0 : expr ℕ -> expr P -> UnderLets (expr P)) (x1 : expr ℕ) =>
    Base
      (#(nat_rect)%expr @ (λ x2 : var unit,
                           to_expr (x ($x2)))%expr @
       (λ (x2 : var ℕ)(x3 : var P),
        to_expr (x0 ($x2) ($x3)))%expr @ x1)%expr_pat
| @nat_rect_arrow P Q =>
    fun (x : expr P -> UnderLets (expr Q))
      (x0 : expr ℕ ->
            (expr P -> UnderLets (expr Q)) -> expr P -> UnderLets (expr Q))
      (x1 : expr ℕ) (x2 : expr P) =>
    Base
      (#(nat_rect_arrow)%expr @ (λ x3 : var P,
                                 to_expr (x ($x3)))%expr @
       (λ (x3 : var ℕ)(x4 : var (P -> Q)%ptype)(x5 : var P),
        to_expr
          (x0 ($x3) (fun x6 : expr P => Base ($x4 @ x6)%expr_pat) ($x5)))%expr @
       x1 @ x2)%expr_pat
| @list_rect A P =>
    fun (x : expr unit -> UnderLets (expr P))
      (x0 : expr A -> expr (list A) -> expr P -> UnderLets (expr P))
      (x1 : expr (list A)) =>
    Base
      (#(list_rect)%expr @ (λ x2 : var unit,
                            to_expr (x ($x2)))%expr @
       (λ (x2 : var A)(x3 : var (list A))(x4 : var P),
        to_expr (x0 ($x2) ($x3) ($x4)))%expr @ x1)%expr_pat
| @list_case A P =>
    fun (x : expr unit -> UnderLets (expr P))
      (x0 : expr A -> expr (list A) -> UnderLets (expr P))
      (x1 : expr (list A)) =>
    Base
      (#(list_case)%expr @ (λ x2 : var unit,
                            to_expr (x ($x2)))%expr @
       (λ (x2 : var A)(x3 : var (list A)),
        to_expr (x0 ($x2) ($x3)))%expr @ x1)%expr_pat
| @List_length T =>
    fun x : expr (list T) => Base (#(List_length)%expr @ x)%expr_pat
| List_seq => fun x x0 : expr ℕ => Base (#(List_seq)%expr @ x @ x0)%expr_pat
| @List_firstn A =>
    fun (x : expr ℕ) (x0 : expr (list A)) =>
    Base (#(List_firstn)%expr @ x @ x0)%expr_pat
| @List_skipn A =>
    fun (x : expr ℕ) (x0 : expr (list A)) =>
    Base (#(List_skipn)%expr @ x @ x0)%expr_pat
| @List_repeat A =>
    fun (x : expr A) (x0 : expr ℕ) =>
    Base (#(List_repeat)%expr @ x @ x0)%expr_pat
| @List_combine A B =>
    fun (x : expr (list A)) (x0 : expr (list B)) =>
    Base (#(List_combine)%expr @ x @ x0)%expr_pat
| @List_map A B =>
    fun (x : expr A -> UnderLets (expr B)) (x0 : expr (list A)) =>
    Base
      (#(List_map)%expr @ (λ x1 : var A,
                           to_expr (x ($x1)))%expr @ x0)%expr_pat
| @List_app A => fun x x0 : expr (list A) => Base (x ++ x0)%expr
| @List_rev A =>
    fun x : expr (list A) => Base (#(List_rev)%expr @ x)%expr_pat
| @List_flat_map A B =>
    fun (x : expr A -> UnderLets (expr (list B))) (x0 : expr (list A)) =>
    Base
      (#(List_flat_map)%expr @ (λ x1 : var A,
                                to_expr (x ($x1)))%expr @ x0)%expr_pat
| @List_partition A =>
    fun (x : expr A -> UnderLets (expr bool)) (x0 : expr (list A)) =>
    Base
      (#(List_partition)%expr @ (λ x1 : var A,
                                 to_expr (x ($x1)))%expr @ x0)%expr_pat
| @List_fold_right A B =>
    fun (x : expr B -> expr A -> UnderLets (expr A)) (x0 : expr A)
      (x1 : expr (list B)) =>
    Base
      (#(List_fold_right)%expr @
       (λ (x2 : var B)(x3 : var A),
        to_expr (x ($x2) ($x3)))%expr @ x0 @ x1)%expr_pat
| @List_update_nth T =>
    fun (x : expr ℕ) (x0 : expr T -> UnderLets (expr T)) (x1 : expr (list T))
    =>
    Base
      (#(List_update_nth)%expr @ x @ (λ x2 : var T,
                                      to_expr (x0 ($x2)))%expr @ x1)%expr_pat
| @List_nth_default T =>
    fun (x : expr T) (x0 : expr (list T)) (x1 : expr ℕ) =>
    Base (#(List_nth_default)%expr @ x @ x0 @ x1)%expr_pat
| Z_add =>
    fun x x0 : expr ℤ =>
    (((match x with
       | @expr.Ident _ _ _ t idc =>
           args <- invert_bind_args idc Raw.ident.Literal;
           match
             pattern.type.unify_extracted (ℤ -> ℤ)%ptype
               ((projT1 args) -> ℤ)%ptype
           with
           | Datatypes.Some (_, _)%zrange =>
               if
                type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                  ((projT1 args) -> ℤ)%ptype
               then
                xv <- ident.unify pattern.ident.Literal ##(projT2 args);
                fv <- (if (let (x1, _) := xv in x1) =? 0
                       then Datatypes.Some (Base x0)
                       else Datatypes.None);
                Datatypes.Some (fv0 <-- fv;
                                Base fv0)%under_lets
               else Datatypes.None
           | Datatypes.None => Datatypes.None
           end
       | _ => Datatypes.None
       end;;
       match x0 with
       | @expr.Ident _ _ _ t idc =>
           args <- invert_bind_args idc Raw.ident.Literal;
           match
             pattern.type.unify_extracted (ℤ -> ℤ)%ptype
               (ℤ -> (projT1 args))%ptype
           with
           | Datatypes.Some (_, _)%zrange =>
               if
                type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                  (ℤ -> (projT1 args))%ptype
               then
                xv <- ident.unify pattern.ident.Literal ##(projT2 args);
                fv <- (if (let (x1, _) := xv in x1) =? 0
                       then Datatypes.Some (Base x)
                       else Datatypes.None);
                Datatypes.Some (fv0 <-- fv;
                                Base fv0)%under_lets
               else Datatypes.None
           | Datatypes.None => Datatypes.None
           end
       | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 =>
           match x with
           | @expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t0 idc0) x2 =>
               _ <- invert_bind_args idc0 Raw.ident.Z_opp;
               _ <- invert_bind_args idc Raw.ident.Z_opp;
               match
                 pattern.type.unify_extracted (ℤ -> ℤ)%ptype (s0 -> s)%ptype
               with
               | Datatypes.Some (_, _)%zrange =>
                   if
                    type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                      (s0 -> s)%ptype
                   then
                    v <- type.try_make_transport_cps s0 ℤ;
                    v0 <- type.try_make_transport_cps s ℤ;
                    Datatypes.Some
                      (Base
                         (-
                          (v (Compile.reflect x2) + v0 (Compile.reflect x1)))%expr)
                   else Datatypes.None
               | Datatypes.None => Datatypes.None
               end
           | @expr.App _ _ _ s0 _ ($_)%expr _ | @expr.App _ _ _ s0 _
             (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s0 _
             (_ @ _)%expr_pat _ | @expr.App _ _ _ s0 _
             (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None
           | _ => Datatypes.None
           end
       | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _
         (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ |
         @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None
       | _ => Datatypes.None
       end;;
       match x with
       | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 =>
           _ <- invert_bind_args idc Raw.ident.Z_opp;
           match
             pattern.type.unify_extracted (ℤ -> ℤ)%ptype (s -> ℤ)%ptype
           with
           | Datatypes.Some (_, _)%zrange =>
               if
                type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                  (s -> ℤ)%ptype
               then
                v <- type.try_make_transport_cps s ℤ;
                Datatypes.Some (Base (x0 - v (Compile.reflect x1))%expr)
               else Datatypes.None
           | Datatypes.None => Datatypes.None
           end
       | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _
         (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ |
         @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None
       | _ => Datatypes.None
       end;;
       match x0 with
       | @expr.Ident _ _ _ t idc =>
           match x with
           | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t0 idc0) x1 =>
               (_ <- invert_bind_args idc0 Raw.ident.Z_opp;
                args0 <- invert_bind_args idc Raw.ident.Literal;
                match
                  pattern.type.unify_extracted (ℤ -> ℤ)%ptype
                    (s -> (projT1 args0))%ptype
                with
                | Datatypes.Some (_, _)%zrange =>
                    if
                     type.type_beq base.type base.type.type_beq
                       (ℤ -> ℤ)%ptype (s -> (projT1 args0))%ptype
                    then
                     v <- type.try_make_transport_cps s ℤ;
                     xv <- ident.unify pattern.ident.Literal ##(projT2 args0);
                     fv <- (if (let (x2, _) := xv in x2) >? 0
                            then
                             Datatypes.Some
                               (Base
                                  (##(let (x2, _) := xv in x2) -
                                   v (Compile.reflect x1))%expr)
                            else Datatypes.None);
                     Datatypes.Some (fv0 <-- fv;
                                     Base fv0)%under_lets
                    else Datatypes.None
                | Datatypes.None => Datatypes.None
                end);;
               _ <- invert_bind_args idc0 Raw.ident.Z_opp;
               args0 <- invert_bind_args idc Raw.ident.Literal;
               match
                 pattern.type.unify_extracted (ℤ -> ℤ)%ptype
                   (s -> (projT1 args0))%ptype
               with
               | Datatypes.Some (_, _)%zrange =>
                   if
                    type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                      (s -> (projT1 args0))%ptype
                   then
                    v <- type.try_make_transport_cps s ℤ;
                    xv <- ident.unify pattern.ident.Literal ##(projT2 args0);
                    fv <- (if (let (x2, _) := xv in x2) <? 0
                           then
                            Datatypes.Some
                              (Base
                                 (-
                                  (v (Compile.reflect x1) +
                                   ##(- (let (x2, _) := xv in x2))%Z))%expr)
                           else Datatypes.None);
                    Datatypes.Some (fv0 <-- fv;
                                    Base fv0)%under_lets
                   else Datatypes.None
               | Datatypes.None => Datatypes.None
               end
           | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _
             (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat
             _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ =>
               Datatypes.None
           | _ => Datatypes.None
           end
       | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 =>
           (_ <- invert_bind_args idc Raw.ident.Z_opp;
            match
              pattern.type.unify_extracted (ℤ -> ℤ)%ptype (ℤ -> s)%ptype
            with
            | Datatypes.Some (_, _)%zrange =>
                if
                 type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                   (ℤ -> s)%ptype
                then
                 v <- type.try_make_transport_cps s ℤ;
                 Datatypes.Some (Base (x - v (Compile.reflect x1))%expr)
                else Datatypes.None
            | Datatypes.None => Datatypes.None
            end);;
           match x with
           | @expr.Ident _ _ _ t0 idc0 =>
               (args <- invert_bind_args idc0 Raw.ident.Literal;
                _ <- invert_bind_args idc Raw.ident.Z_opp;
                match
                  pattern.type.unify_extracted (ℤ -> ℤ)%ptype
                    ((projT1 args) -> s)%ptype
                with
                | Datatypes.Some (_, _)%zrange =>
                    if
                     type.type_beq base.type base.type.type_beq
                       (ℤ -> ℤ)%ptype ((projT1 args) -> s)%ptype
                    then
                     xv <- ident.unify pattern.ident.Literal ##(projT2 args);
                     v <- type.try_make_transport_cps s ℤ;
                     fv <- (if (let (x2, _) := xv in x2) >? 0
                            then
                             Datatypes.Some
                               (Base
                                  (##(let (x2, _) := xv in x2) -
                                   v (Compile.reflect x1))%expr)
                            else Datatypes.None);
                     Datatypes.Some (fv0 <-- fv;
                                     Base fv0)%under_lets
                    else Datatypes.None
                | Datatypes.None => Datatypes.None
                end);;
               args <- invert_bind_args idc0 Raw.ident.Literal;
               _ <- invert_bind_args idc Raw.ident.Z_opp;
               match
                 pattern.type.unify_extracted (ℤ -> ℤ)%ptype
                   ((projT1 args) -> s)%ptype
               with
               | Datatypes.Some (_, _)%zrange =>
                   if
                    type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                      ((projT1 args) -> s)%ptype
                   then
                    xv <- ident.unify pattern.ident.Literal ##(projT2 args);
                    v <- type.try_make_transport_cps s ℤ;
                    fv <- (if (let (x2, _) := xv in x2) <? 0
                           then
                            Datatypes.Some
                              (Base
                                 (-
                                  (##(- (let (x2, _) := xv in x2))%Z +
                                   v (Compile.reflect x1)))%expr)
                           else Datatypes.None);
                    Datatypes.Some (fv0 <-- fv;
                                    Base fv0)%under_lets
                   else Datatypes.None
               | Datatypes.None => Datatypes.None
               end
           | _ => Datatypes.None
           end
       | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _
         (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ |
         @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None
       | _ => Datatypes.None
       end);;
      Datatypes.None);;;
     Base (x + x0)%expr)%option
| Z_mul =>
    fun x x0 : expr ℤ =>
    (((match x with
       | @expr.Ident _ _ _ t idc =>
           args <- invert_bind_args idc Raw.ident.Literal;
           match
             pattern.type.unify_extracted (ℤ -> ℤ)%ptype
               ((projT1 args) -> ℤ)%ptype
           with
           | Datatypes.Some (_, _)%zrange =>
               if
                type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                  ((projT1 args) -> ℤ)%ptype
               then
                xv <- ident.unify pattern.ident.Literal ##(projT2 args);
                fv <- (if (let (x1, _) := xv in x1) =? 0
                       then Datatypes.Some (Base (##0)%expr)
                       else Datatypes.None);
                Datatypes.Some (fv0 <-- fv;
                                Base fv0)%under_lets
               else Datatypes.None
           | Datatypes.None => Datatypes.None
           end
       | _ => Datatypes.None
       end;;
       match x0 with
       | @expr.Ident _ _ _ t idc =>
           args <- invert_bind_args idc Raw.ident.Literal;
           match
             pattern.type.unify_extracted (ℤ -> ℤ)%ptype
               (ℤ -> (projT1 args))%ptype
           with
           | Datatypes.Some (_, _)%zrange =>
               if
                type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                  (ℤ -> (projT1 args))%ptype
               then
                xv <- ident.unify pattern.ident.Literal ##(projT2 args);
                fv <- (if (let (x1, _) := xv in x1) =? 0
                       then Datatypes.Some (Base (##0)%expr)
                       else Datatypes.None);
                Datatypes.Some (fv0 <-- fv;
                                Base fv0)%under_lets
               else Datatypes.None
           | Datatypes.None => Datatypes.None
           end
       | _ => Datatypes.None
       end;;
       match x with
       | @expr.Ident _ _ _ t idc =>
           args <- invert_bind_args idc Raw.ident.Literal;
           match
             pattern.type.unify_extracted (ℤ -> ℤ)%ptype
               ((projT1 args) -> ℤ)%ptype
           with
           | Datatypes.Some (_, _)%zrange =>
               if
                type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                  ((projT1 args) -> ℤ)%ptype
               then
                xv <- ident.unify pattern.ident.Literal ##(projT2 args);
                fv <- (if (let (x1, _) := xv in x1) =? 1
                       then Datatypes.Some (Base x0)
                       else Datatypes.None);
                Datatypes.Some (fv0 <-- fv;
                                Base fv0)%under_lets
               else Datatypes.None
           | Datatypes.None => Datatypes.None
           end
       | _ => Datatypes.None
       end;;
       match x0 with
       | @expr.Ident _ _ _ t idc =>
           (args <- invert_bind_args idc Raw.ident.Literal;
            match
              pattern.type.unify_extracted (ℤ -> ℤ)%ptype
                (ℤ -> (projT1 args))%ptype
            with
            | Datatypes.Some (_, _)%zrange =>
                if
                 type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                   (ℤ -> (projT1 args))%ptype
                then
                 xv <- ident.unify pattern.ident.Literal ##(projT2 args);
                 fv <- (if (let (x1, _) := xv in x1) =? 1
                        then Datatypes.Some (Base x)
                        else Datatypes.None);
                 Datatypes.Some (fv0 <-- fv;
                                 Base fv0)%under_lets
                else Datatypes.None
            | Datatypes.None => Datatypes.None
            end);;
           match x with
           | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t0 idc0) x1 =>
               _ <- invert_bind_args idc0 Raw.ident.Z_opp;
               args0 <- invert_bind_args idc Raw.ident.Literal;
               match
                 pattern.type.unify_extracted (ℤ -> ℤ)%ptype
                   (s -> (projT1 args0))%ptype
               with
               | Datatypes.Some (_, _)%zrange =>
                   if
                    type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                      (s -> (projT1 args0))%ptype
                   then
                    v <- type.try_make_transport_cps s ℤ;
                    xv <- ident.unify pattern.ident.Literal ##(projT2 args0);
                    fv <- (if (let (x2, _) := xv in x2) =? -1
                           then
                            Datatypes.Some (Base (v (Compile.reflect x1)))
                           else Datatypes.None);
                    Datatypes.Some (fv0 <-- fv;
                                    Base fv0)%under_lets
                   else Datatypes.None
               | Datatypes.None => Datatypes.None
               end
           | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _
             (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat
             _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ =>
               Datatypes.None
           | _ => Datatypes.None
           end
       | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 =>
           match x with
           | @expr.Ident _ _ _ t0 idc0 =>
               args <- invert_bind_args idc0 Raw.ident.Literal;
               _ <- invert_bind_args idc Raw.ident.Z_opp;
               match
                 pattern.type.unify_extracted (ℤ -> ℤ)%ptype
                   ((projT1 args) -> s)%ptype
               with
               | Datatypes.Some (_, _)%zrange =>
                   if
                    type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                      ((projT1 args) -> s)%ptype
                   then
                    xv <- ident.unify pattern.ident.Literal ##(projT2 args);
                    v <- type.try_make_transport_cps s ℤ;
                    fv <- (if (let (x2, _) := xv in x2) =? -1
                           then
                            Datatypes.Some (Base (v (Compile.reflect x1)))
                           else Datatypes.None);
                    Datatypes.Some (fv0 <-- fv;
                                    Base fv0)%under_lets
                   else Datatypes.None
               | Datatypes.None => Datatypes.None
               end
           | _ => Datatypes.None
           end
       | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _
         (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ |
         @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None
       | _ => Datatypes.None
       end;;
       match x with
       | @expr.Ident _ _ _ t idc =>
           args <- invert_bind_args idc Raw.ident.Literal;
           match
             pattern.type.unify_extracted (ℤ -> ℤ)%ptype
               ((projT1 args) -> ℤ)%ptype
           with
           | Datatypes.Some (_, _)%zrange =>
               if
                type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                  ((projT1 args) -> ℤ)%ptype
               then
                xv <- ident.unify pattern.ident.Literal ##(projT2 args);
                fv <- (if (let (x1, _) := xv in x1) =? -1
                       then Datatypes.Some (Base (- x0)%expr)
                       else Datatypes.None);
                Datatypes.Some (fv0 <-- fv;
                                Base fv0)%under_lets
               else Datatypes.None
           | Datatypes.None => Datatypes.None
           end
       | _ => Datatypes.None
       end;;
       match x0 with
       | @expr.Ident _ _ _ t idc =>
           args <- invert_bind_args idc Raw.ident.Literal;
           match
             pattern.type.unify_extracted (ℤ -> ℤ)%ptype
               (ℤ -> (projT1 args))%ptype
           with
           | Datatypes.Some (_, _)%zrange =>
               if
                type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                  (ℤ -> (projT1 args))%ptype
               then
                xv <- ident.unify pattern.ident.Literal ##(projT2 args);
                fv <- (if (let (x1, _) := xv in x1) =? -1
                       then Datatypes.Some (Base (- x)%expr)
                       else Datatypes.None);
                Datatypes.Some (fv0 <-- fv;
                                Base fv0)%under_lets
               else Datatypes.None
           | Datatypes.None => Datatypes.None
           end
       | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 =>
           match x with
           | @expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t0 idc0) x2 =>
               _ <- invert_bind_args idc0 Raw.ident.Z_opp;
               _ <- invert_bind_args idc Raw.ident.Z_opp;
               match
                 pattern.type.unify_extracted (ℤ -> ℤ)%ptype (s0 -> s)%ptype
               with
               | Datatypes.Some (_, _)%zrange =>
                   if
                    type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                      (s0 -> s)%ptype
                   then
                    v <- type.try_make_transport_cps s0 ℤ;
                    v0 <- type.try_make_transport_cps s ℤ;
                    Datatypes.Some
                      (Base
                         (v (Compile.reflect x2) * v0 (Compile.reflect x1))%expr)
                   else Datatypes.None
               | Datatypes.None => Datatypes.None
               end
           | @expr.App _ _ _ s0 _ ($_)%expr _ | @expr.App _ _ _ s0 _
             (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s0 _
             (_ @ _)%expr_pat _ | @expr.App _ _ _ s0 _
             (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None
           | _ => Datatypes.None
           end
       | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _
         (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ |
         @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None
       | _ => Datatypes.None
       end;;
       match x with
       | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 =>
           _ <- invert_bind_args idc Raw.ident.Z_opp;
           match
             pattern.type.unify_extracted (ℤ -> ℤ)%ptype (s -> ℤ)%ptype
           with
           | Datatypes.Some (_, _)%zrange =>
               if
                type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                  (s -> ℤ)%ptype
               then
                v <- type.try_make_transport_cps s ℤ;
                Datatypes.Some (Base (- (v (Compile.reflect x1) * x0))%expr)
               else Datatypes.None
           | Datatypes.None => Datatypes.None
           end
       | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _
         (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ |
         @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None
       | _ => Datatypes.None
       end;;
       match x0 with
       | @expr.Ident _ _ _ t idc =>
           match x with
           | @expr.Ident _ _ _ t0 idc0 =>
               args <- invert_bind_args idc0 Raw.ident.Literal;
               args0 <- invert_bind_args idc Raw.ident.Literal;
               match
                 pattern.type.unify_extracted (ℤ -> ℤ)%ptype
                   ((projT1 args) -> (projT1 args0))%ptype
               with
               | Datatypes.Some (_, _)%zrange =>
                   if
                    type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                      ((projT1 args) -> (projT1 args0))%ptype
                   then
                    xv <- ident.unify pattern.ident.Literal ##(projT2 args);
                    xv0 <- ident.unify pattern.ident.Literal ##(projT2 args0);
                    Datatypes.Some
                      (Base
                         (##((let (x1, _) := xv in x1) *
                             (let (x1, _) := xv0 in x1))%Z)%expr)
                   else Datatypes.None
               | Datatypes.None => Datatypes.None
               end
           | _ => Datatypes.None
           end
       | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 =>
           _ <- invert_bind_args idc Raw.ident.Z_opp;
           match
             pattern.type.unify_extracted (ℤ -> ℤ)%ptype (ℤ -> s)%ptype
           with
           | Datatypes.Some (_, _)%zrange =>
               if
                type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                  (ℤ -> s)%ptype
               then
                v <- type.try_make_transport_cps s ℤ;
                Datatypes.Some (Base (- (x * v (Compile.reflect x1)))%expr)
               else Datatypes.None
           | Datatypes.None => Datatypes.None
           end
       | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _
         (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ |
         @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None
       | _ => Datatypes.None
       end;;
       match x with
       | @expr.Ident _ _ _ t idc =>
           args <- invert_bind_args idc Raw.ident.Literal;
           match
             pattern.type.unify_extracted (ℤ -> ℤ)%ptype
               ((projT1 args) -> ℤ)%ptype
           with
           | Datatypes.Some (_, _)%zrange =>
               if
                type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                  ((projT1 args) -> ℤ)%ptype
               then
                xv <- ident.unify pattern.ident.Literal ##(projT2 args);
                fv <- (if (let (x1, _) := xv in x1) <? 0
                       then
                        Datatypes.Some
                          (Base
                             (- (##(- (let (x1, _) := xv in x1))%Z * x0))%expr)
                       else Datatypes.None);
                Datatypes.Some (fv0 <-- fv;
                                Base fv0)%under_lets
               else Datatypes.None
           | Datatypes.None => Datatypes.None
           end
       | _ => Datatypes.None
       end;;
       match x0 with
       | @expr.Ident _ _ _ t idc =>
           (args <- invert_bind_args idc Raw.ident.Literal;
            match
              pattern.type.unify_extracted (ℤ -> ℤ)%ptype
                (ℤ -> (projT1 args))%ptype
            with
            | Datatypes.Some (_, _)%zrange =>
                if
                 type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                   (ℤ -> (projT1 args))%ptype
                then
                 xv <- ident.unify pattern.ident.Literal ##(projT2 args);
                 fv <- (if (let (x1, _) := xv in x1) <? 0
                        then
                         Datatypes.Some
                           (Base
                              (- (x * ##(- (let (x1, _) := xv in x1))%Z))%expr)
                        else Datatypes.None);
                 Datatypes.Some (fv0 <-- fv;
                                 Base fv0)%under_lets
                else Datatypes.None
            | Datatypes.None => Datatypes.None
            end);;
           args <- invert_bind_args idc Raw.ident.Literal;
           match
             pattern.type.unify_extracted (ℤ -> ℤ)%ptype
               (ℤ -> (projT1 args))%ptype
           with
           | Datatypes.Some (_, _)%zrange =>
               if
                type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                  (ℤ -> (projT1 args))%ptype
               then
                xv <- ident.unify pattern.ident.Literal ##(projT2 args);
                fv <- (if
                        ((let (x1, _) := xv in x1) =?
                         2 ^ Z.log2 (let (x1, _) := xv in x1)) &&
                        negb ((let (x1, _) := xv in x1) =? 2)
                       then
                        Datatypes.Some
                          (Base
                             (x << ##(Z.log2 (let (x1, _) := xv in x1)))%expr)
                       else Datatypes.None);
                Datatypes.Some (fv0 <-- fv;
                                Base fv0)%under_lets
               else Datatypes.None
           | Datatypes.None => Datatypes.None
           end
       | _ => Datatypes.None
       end;;
       match x with
       | @expr.Ident _ _ _ t idc =>
           (args <- invert_bind_args idc Raw.ident.Literal;
            match
              pattern.type.unify_extracted (ℤ -> ℤ)%ptype
                ((projT1 args) -> ℤ)%ptype
            with
            | Datatypes.Some (_, _)%zrange =>
                if
                 type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                   ((projT1 args) -> ℤ)%ptype
                then
                 xv <- ident.unify pattern.ident.Literal ##(projT2 args);
                 fv <- (if
                         ((let (x1, _) := xv in x1) =?
                          2 ^ Z.log2 (let (x1, _) := xv in x1)) &&
                         negb ((let (x1, _) := xv in x1) =? 2)
                        then
                         Datatypes.Some
                           (Base
                              (x0 << ##(Z.log2 (let (x1, _) := xv in x1)))%expr)
                        else Datatypes.None);
                 Datatypes.Some (fv0 <-- fv;
                                 Base fv0)%under_lets
                else Datatypes.None
            | Datatypes.None => Datatypes.None
            end);;
           match x0 with
           | @expr.App _ _ _ s _
             (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t0 idc0) x2) x1 =>
               match x2 with
               | @expr.Ident _ _ _ t1 idc1 =>
                   match x1 with
                   | @expr.App _ _ _ s1 _
                     (@expr.App _ _ _ s2 _ (@expr.Ident _ _ _ t2 idc2) x4)
                     x3 =>
                       _ <- invert_bind_args idc2 Raw.ident.Z_mul;
                       args0 <- invert_bind_args idc1 Raw.ident.Literal;
                       _ <- invert_bind_args idc0 Raw.ident.Z_mul;
                       args2 <- invert_bind_args idc Raw.ident.Literal;
                       match
                         pattern.type.unify_extracted
                           (ℤ -> ℤ -> ℤ -> ℤ)%ptype
                           ((projT1 args2) -> (projT1 args0) -> s2 -> s1)%ptype
                       with
                       | Datatypes.Some (_, (_, (_, _)))%zrange =>
                           if
                            type.type_beq base.type base.type.type_beq
                              (ℤ -> ℤ -> ℤ -> ℤ)%ptype
                              ((projT1 args2) -> (projT1 args0) -> s2 -> s1)%ptype
                           then
                            xv <- ident.unify pattern.ident.Literal
                                    ##(projT2 args2);
                            xv0 <- ident.unify pattern.ident.Literal
                                     ##(projT2 args0);
                            v <- type.try_make_transport_cps s2 ℤ;
                            v0 <- type.try_make_transport_cps s1 ℤ;
                            fv <- (if
                                    (Z.abs (let (x5, _) := xv in x5) <=?
                                     Z.abs max_const_val) &&
                                    (Z.abs (let (x5, _) := xv0 in x5) <=?
                                     Z.abs max_const_val)
                                   then
                                    Datatypes.Some
                                      (Base
                                         (v (Compile.reflect x4) *
                                          (v0 (Compile.reflect x3) *
                                           (##(let (x5, _) := xv in x5) *
                                            ##(let (x5, _) := xv0 in x5))))%expr)
                                   else Datatypes.None);
                            Datatypes.Some (fv0 <-- fv;
                                            Base fv0)%under_lets
                           else Datatypes.None
                       | Datatypes.None => Datatypes.None
                       end
                   | @expr.App _ _ _ s1 _ (@expr.App _ _ _ s2 _ ($_)%expr _)
                     _ | @expr.App _ _ _ s1 _
                     (@expr.App _ _ _ s2 _ (@expr.Abs _ _ _ _ _ _) _) _ |
                     @expr.App _ _ _ s1 _
                     (@expr.App _ _ _ s2 _ (_ @ _)%expr_pat _) _ | @expr.App
                     _ _ _ s1 _
                     (@expr.App _ _ _ s2 _ (@expr.LetIn _ _ _ _ _ _ _) _)
                     _ => Datatypes.None
                   | @expr.App _ _ _ s1 _ #(_)%expr_pat _ | @expr.App _ _ _
                     s1 _ ($_)%expr _ | @expr.App _ _ _ s1 _
                     (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s1 _
                     (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None
                   | _ => Datatypes.None
                   end
               | _ => Datatypes.None
               end;;
               match x1 with
               | (@expr.App _ _ _ s2 _ (@expr.Ident _ _ _ t1 idc1) x4 @
                  @expr.Ident _ _ _ t2 idc2)%expr_pat =>
                   args <- invert_bind_args idc2 Raw.ident.Literal;
                   _ <- invert_bind_args idc1 Raw.ident.Z_mul;
                   _ <- invert_bind_args idc0 Raw.ident.Z_mul;
                   args2 <- invert_bind_args idc Raw.ident.Literal;
                   match
                     pattern.type.unify_extracted (ℤ -> ℤ -> ℤ -> ℤ)%ptype
                       ((projT1 args2) -> s0 -> s2 -> (projT1 args))%ptype
                   with
                   | Datatypes.Some (_, (_, (_, _)))%zrange =>
                       if
                        type.type_beq base.type base.type.type_beq
                          (ℤ -> ℤ -> ℤ -> ℤ)%ptype
                          ((projT1 args2) -> s0 -> s2 -> (projT1 args))%ptype
                       then
                        xv <- ident.unify pattern.ident.Literal
                                ##(projT2 args2);
                        v <- type.try_make_transport_cps s0 ℤ;
                        v0 <- type.try_make_transport_cps s2 ℤ;
                        xv0 <- ident.unify pattern.ident.Literal
                                 ##(projT2 args);
                        fv <- (if
                                (Z.abs (let (x5, _) := xv in x5) <=?
                                 Z.abs max_const_val) &&
                                (Z.abs (let (x5, _) := xv0 in x5) <=?
                                 Z.abs max_const_val)
                               then
                                Datatypes.Some
                                  (Base
                                     (v (Compile.reflect x2) *
                                      (v0 (Compile.reflect x4) *
                                       (##(let (x5, _) := xv in x5) *
                                        ##(let (x5, _) := xv0 in x5))))%expr)
                               else Datatypes.None);
                        Datatypes.Some (fv0 <-- fv;
                                        Base fv0)%under_lets
                       else Datatypes.None
                   | Datatypes.None => Datatypes.None
                   end
               | (@expr.App _ _ _ s2 _ (@expr.Ident _ _ _ t1 idc1) x4 @
                  ($_)%expr)%expr_pat |
                 (@expr.App _ _ _ s2 _ (@expr.Ident _ _ _ t1 idc1) x4 @
                  @expr.Abs _ _ _ _ _ _)%expr_pat |
                 (@expr.App _ _ _ s2 _ (@expr.Ident _ _ _ t1 idc1) x4 @
                  (_ @ _))%expr_pat |
                 (@expr.App _ _ _ s2 _ (@expr.Ident _ _ _ t1 idc1) x4 @
                  @expr.LetIn _ _ _ _ _ _ _)%expr_pat => Datatypes.None
               | (@expr.App _ _ _ s2 _ ($_)%expr _ @ _)%expr_pat |
                 (@expr.App _ _ _ s2 _ (@expr.Abs _ _ _ _ _ _) _ @ _)%expr_pat |
                 (@expr.App _ _ _ s2 _ (_ @ _) _ @ _)%expr_pat |
                 (@expr.App _ _ _ s2 _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _)%expr_pat =>
                   Datatypes.None
               | _ => Datatypes.None
               end;;
               _ <- invert_bind_args idc0 Raw.ident.Z_mul;
               args0 <- invert_bind_args idc Raw.ident.Literal;
               match
                 pattern.type.unify_extracted (ℤ -> ℤ -> ℤ)%ptype
                   ((projT1 args0) -> s0 -> s)%ptype
               with
               | Datatypes.Some (_, (_, _))%zrange =>
                   if
                    type.type_beq base.type base.type.type_beq
                      (ℤ -> ℤ -> ℤ)%ptype ((projT1 args0) -> s0 -> s)%ptype
                   then
                    xv <- ident.unify pattern.ident.Literal ##(projT2 args0);
                    v <- type.try_make_transport_cps s0 ℤ;
                    v0 <- type.try_make_transport_cps s ℤ;
                    fv <- (if
                            Z.abs (let (x3, _) := xv in x3) <=?
                            Z.abs max_const_val
                           then
                            Datatypes.Some
                              (Base
                                 (v (Compile.reflect x2) *
                                  (v0 (Compile.reflect x1) *
                                   ##(let (x3, _) := xv in x3)))%expr)
                           else Datatypes.None);
                    Datatypes.Some (fv0 <-- fv;
                                    Base fv0)%under_lets
                   else Datatypes.None
               | Datatypes.None => Datatypes.None
               end
           | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ |
             @expr.App _ _ _ s _
             (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ | @expr.App _
             _ _ s _ (@expr.App _ _ _ s0 _ (_ @ _)%expr_pat _) _ | @expr.App
             _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.LetIn _ _ _ _ _ _ _) _)
             _ => Datatypes.None
           | @expr.App _ _ _ s _ #(_)%expr_pat _ | @expr.App _ _ _ s _
             ($_)%expr _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ |
             @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ =>
               Datatypes.None
           | _ => Datatypes.None
           end;;
           args <- invert_bind_args idc Raw.ident.Literal;
           match
             pattern.type.unify_extracted (ℤ -> ℤ)%ptype
               ((projT1 args) -> ℤ)%ptype
           with
           | Datatypes.Some (_, _)%zrange =>
               if
                type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                  ((projT1 args) -> ℤ)%ptype
               then
                xv <- ident.unify pattern.ident.Literal ##(projT2 args);
                fv <- (if
                        Z.abs (let (x1, _) := xv in x1) <=?
                        Z.abs max_const_val
                       then
                        Datatypes.Some
                          (Base (x0 * ##(let (x1, _) := xv in x1))%expr)
                       else Datatypes.None);
                Datatypes.Some (fv0 <-- fv;
                                Base fv0)%under_lets
               else Datatypes.None
           | Datatypes.None => Datatypes.None
           end
       | _ => Datatypes.None
       end);;
      Datatypes.None);;;
     Base (x * x0)%expr)%option
| Z_pow => fun x x0 : expr ℤ => Base (#(Z_pow)%expr @ x @ x0)%expr_pat
| Z_sub =>
    fun x x0 : expr ℤ =>
    (((match x with
       | @expr.Ident _ _ _ t idc =>
           match x0 with
           | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t0 idc0) x1 =>
               _ <- invert_bind_args idc0 Raw.ident.Z_opp;
               args0 <- invert_bind_args idc Raw.ident.Literal;
               match
                 pattern.type.unify_extracted (ℤ -> ℤ)%ptype
                   ((projT1 args0) -> s)%ptype
               with
               | Datatypes.Some (_, _)%zrange =>
                   if
                    type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                      ((projT1 args0) -> s)%ptype
                   then
                    xv <- ident.unify pattern.ident.Literal ##(projT2 args0);
                    v <- type.try_make_transport_cps s ℤ;
                    fv <- (if (let (x2, _) := xv in x2) =? 0
                           then
                            Datatypes.Some (Base (v (Compile.reflect x1)))
                           else Datatypes.None);
                    Datatypes.Some (fv0 <-- fv;
                                    Base fv0)%under_lets
                   else Datatypes.None
               | Datatypes.None => Datatypes.None
               end
           | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _
             (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat
             _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ =>
               Datatypes.None
           | _ => Datatypes.None
           end;;
           args <- invert_bind_args idc Raw.ident.Literal;
           match
             pattern.type.unify_extracted (ℤ -> ℤ)%ptype
               ((projT1 args) -> ℤ)%ptype
           with
           | Datatypes.Some (_, _)%zrange =>
               if
                type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                  ((projT1 args) -> ℤ)%ptype
               then
                xv <- ident.unify pattern.ident.Literal ##(projT2 args);
                fv <- (if (let (x1, _) := xv in x1) =? 0
                       then Datatypes.Some (Base (- x0)%expr)
                       else Datatypes.None);
                Datatypes.Some (fv0 <-- fv;
                                Base fv0)%under_lets
               else Datatypes.None
           | Datatypes.None => Datatypes.None
           end
       | _ => Datatypes.None
       end;;
       match x0 with
       | @expr.Ident _ _ _ t idc =>
           args <- invert_bind_args idc Raw.ident.Literal;
           match
             pattern.type.unify_extracted (ℤ -> ℤ)%ptype
               (ℤ -> (projT1 args))%ptype
           with
           | Datatypes.Some (_, _)%zrange =>
               if
                type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                  (ℤ -> (projT1 args))%ptype
               then
                xv <- ident.unify pattern.ident.Literal ##(projT2 args);
                fv <- (if (let (x1, _) := xv in x1) =? 0
                       then Datatypes.Some (Base x)
                       else Datatypes.None);
                Datatypes.Some (fv0 <-- fv;
                                Base fv0)%under_lets
               else Datatypes.None
           | Datatypes.None => Datatypes.None
           end
       | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 =>
           match x with
           | @expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t0 idc0) x2 =>
               _ <- invert_bind_args idc0 Raw.ident.Z_opp;
               _ <- invert_bind_args idc Raw.ident.Z_opp;
               match
                 pattern.type.unify_extracted (ℤ -> ℤ)%ptype (s0 -> s)%ptype
               with
               | Datatypes.Some (_, _)%zrange =>
                   if
                    type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                      (s0 -> s)%ptype
                   then
                    v <- type.try_make_transport_cps s0 ℤ;
                    v0 <- type.try_make_transport_cps s ℤ;
                    Datatypes.Some
                      (Base
                         (v0 (Compile.reflect x1) - v (Compile.reflect x2))%expr)
                   else Datatypes.None
               | Datatypes.None => Datatypes.None
               end
           | @expr.App _ _ _ s0 _ ($_)%expr _ | @expr.App _ _ _ s0 _
             (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s0 _
             (_ @ _)%expr_pat _ | @expr.App _ _ _ s0 _
             (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None
           | _ => Datatypes.None
           end
       | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _
         (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ |
         @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None
       | _ => Datatypes.None
       end;;
       match x with
       | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 =>
           _ <- invert_bind_args idc Raw.ident.Z_opp;
           match
             pattern.type.unify_extracted (ℤ -> ℤ)%ptype (s -> ℤ)%ptype
           with
           | Datatypes.Some (_, _)%zrange =>
               if
                type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                  (s -> ℤ)%ptype
               then
                v <- type.try_make_transport_cps s ℤ;
                Datatypes.Some (Base (- (v (Compile.reflect x1) + x0))%expr)
               else Datatypes.None
           | Datatypes.None => Datatypes.None
           end
       | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _
         (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ |
         @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None
       | _ => Datatypes.None
       end;;
       match x0 with
       | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 =>
           (_ <- invert_bind_args idc Raw.ident.Z_opp;
            match
              pattern.type.unify_extracted (ℤ -> ℤ)%ptype (ℤ -> s)%ptype
            with
            | Datatypes.Some (_, _)%zrange =>
                if
                 type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                   (ℤ -> s)%ptype
                then
                 v <- type.try_make_transport_cps s ℤ;
                 Datatypes.Some (Base (x + v (Compile.reflect x1))%expr)
                else Datatypes.None
            | Datatypes.None => Datatypes.None
            end);;
           match x with
           | @expr.Ident _ _ _ t0 idc0 =>
               (args <- invert_bind_args idc0 Raw.ident.Literal;
                _ <- invert_bind_args idc Raw.ident.Z_opp;
                match
                  pattern.type.unify_extracted (ℤ -> ℤ)%ptype
                    ((projT1 args) -> s)%ptype
                with
                | Datatypes.Some (_, _)%zrange =>
                    if
                     type.type_beq base.type base.type.type_beq
                       (ℤ -> ℤ)%ptype ((projT1 args) -> s)%ptype
                    then
                     xv <- ident.unify pattern.ident.Literal ##(projT2 args);
                     v <- type.try_make_transport_cps s ℤ;
                     fv <- (if (let (x2, _) := xv in x2) >? 0
                            then
                             Datatypes.Some
                               (Base
                                  (##(let (x2, _) := xv in x2) +
                                   v (Compile.reflect x1))%expr)
                            else Datatypes.None);
                     Datatypes.Some (fv0 <-- fv;
                                     Base fv0)%under_lets
                    else Datatypes.None
                | Datatypes.None => Datatypes.None
                end);;
               args <- invert_bind_args idc0 Raw.ident.Literal;
               _ <- invert_bind_args idc Raw.ident.Z_opp;
               match
                 pattern.type.unify_extracted (ℤ -> ℤ)%ptype
                   ((projT1 args) -> s)%ptype
               with
               | Datatypes.Some (_, _)%zrange =>
                   if
                    type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                      ((projT1 args) -> s)%ptype
                   then
                    xv <- ident.unify pattern.ident.Literal ##(projT2 args);
                    v <- type.try_make_transport_cps s ℤ;
                    fv <- (if (let (x2, _) := xv in x2) <? 0
                           then
                            Datatypes.Some
                              (Base
                                 (v (Compile.reflect x1) -
                                  ##(- (let (x2, _) := xv in x2))%Z)%expr)
                           else Datatypes.None);
                    Datatypes.Some (fv0 <-- fv;
                                    Base fv0)%under_lets
                   else Datatypes.None
               | Datatypes.None => Datatypes.None
               end
           | _ => Datatypes.None
           end
       | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _
         (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ |
         @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None
       | _ => Datatypes.None
       end;;
       match x with
       | @expr.Ident _ _ _ t idc =>
           args <- invert_bind_args idc Raw.ident.Literal;
           match
             pattern.type.unify_extracted (ℤ -> ℤ)%ptype
               ((projT1 args) -> ℤ)%ptype
           with
           | Datatypes.Some (_, _)%zrange =>
               if
                type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                  ((projT1 args) -> ℤ)%ptype
               then
                xv <- ident.unify pattern.ident.Literal ##(projT2 args);
                fv <- (if (let (x1, _) := xv in x1) <? 0
                       then
                        Datatypes.Some
                          (Base
                             (- (##(- (let (x1, _) := xv in x1))%Z + x0))%expr)
                       else Datatypes.None);
                Datatypes.Some (fv0 <-- fv;
                                Base fv0)%under_lets
               else Datatypes.None
           | Datatypes.None => Datatypes.None
           end
       | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 =>
           match x0 with
           | @expr.Ident _ _ _ t0 idc0 =>
               (args <- invert_bind_args idc0 Raw.ident.Literal;
                _ <- invert_bind_args idc Raw.ident.Z_opp;
                match
                  pattern.type.unify_extracted (ℤ -> ℤ)%ptype
                    (s -> (projT1 args))%ptype
                with
                | Datatypes.Some (_, _)%zrange =>
                    if
                     type.type_beq base.type base.type.type_beq
                       (ℤ -> ℤ)%ptype (s -> (projT1 args))%ptype
                    then
                     v <- type.try_make_transport_cps s ℤ;
                     xv <- ident.unify pattern.ident.Literal ##(projT2 args);
                     fv <- (if (let (x2, _) := xv in x2) >? 0
                            then
                             Datatypes.Some
                               (Base
                                  (-
                                   (v (Compile.reflect x1) +
                                    ##(let (x2, _) := xv in x2)))%expr)
                            else Datatypes.None);
                     Datatypes.Some (fv0 <-- fv;
                                     Base fv0)%under_lets
                    else Datatypes.None
                | Datatypes.None => Datatypes.None
                end);;
               args <- invert_bind_args idc0 Raw.ident.Literal;
               _ <- invert_bind_args idc Raw.ident.Z_opp;
               match
                 pattern.type.unify_extracted (ℤ -> ℤ)%ptype
                   (s -> (projT1 args))%ptype
               with
               | Datatypes.Some (_, _)%zrange =>
                   if
                    type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                      (s -> (projT1 args))%ptype
                   then
                    v <- type.try_make_transport_cps s ℤ;
                    xv <- ident.unify pattern.ident.Literal ##(projT2 args);
                    fv <- (if (let (x2, _) := xv in x2) <? 0
                           then
                            Datatypes.Some
                              (Base
                                 (##(- (let (x2, _) := xv in x2))%Z -
                                  v (Compile.reflect x1))%expr)
                           else Datatypes.None);
                    Datatypes.Some (fv0 <-- fv;
                                    Base fv0)%under_lets
                   else Datatypes.None
               | Datatypes.None => Datatypes.None
               end
           | _ => Datatypes.None
           end
       | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _
         (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ |
         @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None
       | _ => Datatypes.None
       end;;
       match x0 with
       | @expr.Ident _ _ _ t idc =>
           args <- invert_bind_args idc Raw.ident.Literal;
           match
             pattern.type.unify_extracted (ℤ -> ℤ)%ptype
               (ℤ -> (projT1 args))%ptype
           with
           | Datatypes.Some (_, _)%zrange =>
               if
                type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                  (ℤ -> (projT1 args))%ptype
               then
                xv <- ident.unify pattern.ident.Literal ##(projT2 args);
                fv <- (if (let (x1, _) := xv in x1) <? 0
                       then
                        Datatypes.Some
                          (Base (x + ##(- (let (x1, _) := xv in x1))%Z)%expr)
                       else Datatypes.None);
                Datatypes.Some (fv0 <-- fv;
                                Base fv0)%under_lets
               else Datatypes.None
           | Datatypes.None => Datatypes.None
           end
       | _ => Datatypes.None
       end);;
      Datatypes.None);;;
     Base (x - x0)%expr)%option
| Z_opp =>
    fun x : expr ℤ =>
    (((match x with
       | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x0 =>
           _ <- invert_bind_args idc Raw.ident.Z_opp;
           match pattern.type.unify_extracted ℤ s with
           | Datatypes.Some _ =>
               if type.type_beq base.type base.type.type_beq ℤ s
               then
                v <- type.try_make_transport_cps s ℤ;
                Datatypes.Some (Base (v (Compile.reflect x0)))
               else Datatypes.None
           | Datatypes.None => Datatypes.None
           end
       | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _
         (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ |
         @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None
       | _ => Datatypes.None
       end;;
       match pattern.type.unify_extracted ℤ ℤ with
       | Datatypes.Some _ =>
           if type.type_beq base.type base.type.type_beq ℤ ℤ
           then
            fv <- (if negb (SubstVarLike.is_var_fst_snd_pair_opp_cast x)
                   then
                    Datatypes.Some
                      (UnderLet x (fun v : var ℤ => Base (- $v)%expr))
                   else Datatypes.None);
            Datatypes.Some (fv0 <-- fv;
                            Base fv0)%under_lets
           else Datatypes.None
       | Datatypes.None => Datatypes.None
       end);;
      Datatypes.None);;;
     Base (- x)%expr)%option
| Z_div =>
    fun x x0 : expr ℤ =>
    ((match x0 with
      | @expr.Ident _ _ _ t idc =>
          (args <- invert_bind_args idc Raw.ident.Literal;
           match
             pattern.type.unify_extracted (ℤ -> ℤ)%ptype
               (ℤ -> (projT1 args))%ptype
           with
           | Datatypes.Some (_, _)%zrange =>
               if
                type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                  (ℤ -> (projT1 args))%ptype
               then
                xv <- ident.unify pattern.ident.Literal ##(projT2 args);
                fv <- (if (let (x1, _) := xv in x1) =? 1
                       then Datatypes.Some (Base x)
                       else Datatypes.None);
                Datatypes.Some (fv0 <-- fv;
                                Base fv0)%under_lets
               else Datatypes.None
           | Datatypes.None => Datatypes.None
           end);;
          args <- invert_bind_args idc Raw.ident.Literal;
          match
            pattern.type.unify_extracted (ℤ -> ℤ)%ptype
              (ℤ -> (projT1 args))%ptype
          with
          | Datatypes.Some (_, _)%zrange =>
              if
               type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                 (ℤ -> (projT1 args))%ptype
              then
               xv <- ident.unify pattern.ident.Literal ##(projT2 args);
               fv <- (if
                       (let (x1, _) := xv in x1) =?
                       2 ^ Z.log2 (let (x1, _) := xv in x1)
                      then
                       Datatypes.Some
                         (Base
                            (x >> ##(Z.log2 (let (x1, _) := xv in x1)))%expr)
                      else Datatypes.None);
               Datatypes.Some (fv0 <-- fv;
                               Base fv0)%under_lets
              else Datatypes.None
          | Datatypes.None => Datatypes.None
          end
      | _ => Datatypes.None
      end;;
      Datatypes.None);;;
     Base (x / x0)%expr)%option
| Z_modulo =>
    fun x x0 : expr ℤ =>
    (match x0 with
     | @expr.Ident _ _ _ t idc =>
         (args <- invert_bind_args idc Raw.ident.Literal;
          match
            pattern.type.unify_extracted (ℤ -> ℤ)%ptype
              (ℤ -> (projT1 args))%ptype
          with
          | Datatypes.Some (_, _)%zrange =>
              if
               type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                 (ℤ -> (projT1 args))%ptype
              then
               xv <- ident.unify pattern.ident.Literal ##(projT2 args);
               fv <- (if (let (x1, _) := xv in x1) =? 1
                      then Datatypes.Some (Base (##0)%expr)
                      else Datatypes.None);
               Datatypes.Some (fv0 <-- fv;
                               Base fv0)%under_lets
              else Datatypes.None
          | Datatypes.None => Datatypes.None
          end);;
         args <- invert_bind_args idc Raw.ident.Literal;
         match
           pattern.type.unify_extracted (ℤ -> ℤ)%ptype
             (ℤ -> (projT1 args))%ptype
         with
         | Datatypes.Some (_, _)%zrange =>
             if
              type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                (ℤ -> (projT1 args))%ptype
             then
              xv <- ident.unify pattern.ident.Literal ##(projT2 args);
              fv <- (if
                      (let (x1, _) := xv in x1) =?
                      2 ^ Z.log2 (let (x1, _) := xv in x1)
                     then
                      Datatypes.Some
                        (Base (x &' ##((let (x1, _) := xv in x1) - 1)%Z)%expr)
                     else Datatypes.None);
              Datatypes.Some (fv0 <-- fv;
                              Base fv0)%under_lets
             else Datatypes.None
         | Datatypes.None => Datatypes.None
         end
     | _ => Datatypes.None
     end;;;
     Base (x mod x0)%expr)%option
| Z_log2 => fun x : expr ℤ => Base (#(Z_log2)%expr @ x)%expr_pat
| Z_log2_up => fun x : expr ℤ => Base (#(Z_log2_up)%expr @ x)%expr_pat
| Z_eqb => fun x x0 : expr ℤ => Base (#(Z_eqb)%expr @ x @ x0)%expr_pat
| Z_leb => fun x x0 : expr ℤ => Base (#(Z_leb)%expr @ x @ x0)%expr_pat
| Z_ltb => fun x x0 : expr ℤ => Base (#(Z_ltb)%expr @ x @ x0)%expr_pat
| Z_geb => fun x x0 : expr ℤ => Base (#(Z_geb)%expr @ x @ x0)%expr_pat
| Z_gtb => fun x x0 : expr ℤ => Base (#(Z_gtb)%expr @ x @ x0)%expr_pat
| Z_of_nat => fun x : expr ℕ => Base (#(Z_of_nat)%expr @ x)%expr_pat
| Z_to_nat => fun x : expr ℤ => Base (#(Z_to_nat)%expr @ x)%expr_pat
| Z_shiftr => fun x x0 : expr ℤ => Base (x >> x0)%expr
| Z_shiftl => fun x x0 : expr ℤ => Base (x << x0)%expr
| Z_land =>
    fun x x0 : expr ℤ =>
    ((match x0 with
      | @expr.Ident _ _ _ t idc =>
          args <- invert_bind_args idc Raw.ident.Literal;
          match
            pattern.type.unify_extracted (ℤ -> ℤ)%ptype
              (ℤ -> (projT1 args))%ptype
          with
          | Datatypes.Some (_, _)%zrange =>
              if
               type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
                 (ℤ -> (projT1 args))%ptype
              then
               xv <- ident.unify pattern.ident.Literal ##(projT2 args);
               fv <- (if (let (x1, _) := xv in x1) =? 0
                      then Datatypes.Some (Base (##0)%expr)
                      else Datatypes.None);
               Datatypes.Some (fv0 <-- fv;
                               Base fv0)%under_lets
              else Datatypes.None
          | Datatypes.None => Datatypes.None
          end
      | _ => Datatypes.None
      end;;
      Datatypes.None);;;
     Base (x &' x0)%expr)%option
| Z_lor => fun x x0 : expr ℤ => Base (x || x0)%expr
| Z_min => fun x x0 : expr ℤ => Base (#(Z_min)%expr @ x @ x0)%expr_pat
| Z_max => fun x x0 : expr ℤ => Base (#(Z_max)%expr @ x @ x0)%expr_pat
| Z_bneg => fun x : expr ℤ => Base (#(Z_bneg)%expr @ x)%expr_pat
| Z_lnot_modulo =>
    fun x x0 : expr ℤ => Base (#(Z_lnot_modulo)%expr @ x @ x0)%expr_pat
| Z_mul_split =>
    fun x x0 x1 : expr ℤ => Base (#(Z_mul_split)%expr @ x @ x0 @ x1)%expr_pat
| Z_add_get_carry =>
    fun x x0 x1 : expr ℤ =>
    Base (#(Z_add_get_carry)%expr @ x @ x0 @ x1)%expr_pat
| Z_add_with_carry =>
    fun x x0 x1 : expr ℤ =>
    Base (#(Z_add_with_carry)%expr @ x @ x0 @ x1)%expr_pat
| Z_add_with_get_carry =>
    fun x x0 x1 x2 : expr ℤ =>
    Base (#(Z_add_with_get_carry)%expr @ x @ x0 @ x1 @ x2)%expr_pat
| Z_sub_get_borrow =>
    fun x x0 x1 : expr ℤ =>
    Base (#(Z_sub_get_borrow)%expr @ x @ x0 @ x1)%expr_pat
| Z_sub_with_get_borrow =>
    fun x x0 x1 x2 : expr ℤ =>
    Base (#(Z_sub_with_get_borrow)%expr @ x @ x0 @ x1 @ x2)%expr_pat
| Z_zselect =>
    fun x x0 x1 : expr ℤ => Base (#(Z_zselect)%expr @ x @ x0 @ x1)%expr_pat
| Z_add_modulo =>
    fun x x0 x1 : expr ℤ =>
    Base (#(Z_add_modulo)%expr @ x @ x0 @ x1)%expr_pat
| Z_rshi =>
    fun x x0 x1 x2 : expr ℤ =>
    Base (#(Z_rshi)%expr @ x @ x0 @ x1 @ x2)%expr_pat
| Z_cc_m => fun x x0 : expr ℤ => Base (#(Z_cc_m)%expr @ x @ x0)%expr_pat
| Z_cast range => fun x : expr ℤ => Base (#(Z_cast range)%expr @ x)%expr_pat
| Z_cast2 range =>
    fun x : expr (ℤ * ℤ)%etype =>
    (match x with
     | @expr.App _ _ _ s _
       (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) x1) x0 =>
         args <- invert_bind_args idc Raw.ident.pair;
         match
           pattern.type.unify_extracted
             (((ℤ -> ℤ -> (ℤ * ℤ)%pbtype) -> ℤ) -> ℤ)%ptype
             ((((let (x2, _) := args in x2) ->
                (let (_, y) := args in y) ->
                ((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) ->
               s0) -> s)%ptype
         with
         | Datatypes.Some (_, (_, (_, _)), _, _)%zrange =>
             if
              type.type_beq base.type base.type.type_beq
                (((ℤ -> ℤ -> (ℤ * ℤ)%etype) -> ℤ) -> ℤ)%ptype
                ((((let (x2, _) := args in x2) ->
                   (let (_, y) := args in y) ->
                   ((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) ->
                  s0) -> s)%ptype
             then
              _ <- ident.unify pattern.ident.pair pair;
              v <- type.try_make_transport_cps s0 ℤ;
              v0 <- type.try_make_transport_cps s ℤ;
              Datatypes.Some
                (fv0 <-- do_again (ℤ * ℤ)
                           (#(Z_cast (Datatypes.fst range))%expr @
                            ($(v (Compile.reflect x1)))%expr,
                           #(Z_cast (Datatypes.snd range))%expr @
                           ($(v0 (Compile.reflect x0)))%expr)%expr_pat;
                 Base fv0)%under_lets
             else Datatypes.None
         | Datatypes.None => Datatypes.None
         end
     | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App _
       _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ | @expr.App
       _ _ _ s _ (@expr.App _ _ _ s0 _ (_ @ _)%expr_pat _) _ | @expr.App _ _
       _ s _ (@expr.App _ _ _ s0 _ (@expr.LetIn _ _ _ _ _ _ _) _) _ =>
         Datatypes.None
     | @expr.App _ _ _ s _ #(_)%expr_pat _ | @expr.App _ _ _ s _ ($_)%expr
       _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s
       _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None
     | _ => Datatypes.None
     end;;;
     Base (#(Z_cast2 range)%expr @ x)%expr_pat)%option
| Some A => fun x : expr A => Base (#(Some)%expr @ x)%expr_pat
| None A => Base #(None)%expr
| @option_rect A P =>
    fun (x : expr A -> UnderLets (expr P))
      (x0 : expr unit -> UnderLets (expr P)) (x1 : expr (base.type.option A))
    =>
    Base
      (#(option_rect)%expr @ (λ x2 : var A,
                              to_expr (x ($x2)))%expr @
       (λ x2 : var unit,
        to_expr (x0 ($x2)))%expr @ x1)%expr_pat
| Build_zrange =>
    fun x x0 : expr ℤ => Base (#(Build_zrange)%expr @ x @ x0)%expr_pat
| @zrange_rect P =>
    fun (x : expr ℤ -> expr ℤ -> UnderLets (expr P))
      (x0 : expr base.type.zrange) =>
    Base
      (#(zrange_rect)%expr @ (λ x1 x2 : var ℤ,
                              to_expr (x ($x1) ($x2)))%expr @ x0)%expr_pat
| fancy_add log2wordmax imm =>
    fun x : expr (ℤ * ℤ)%etype =>
    Base (#(fancy_add log2wordmax imm)%expr @ x)%expr_pat
| fancy_addc log2wordmax imm =>
    fun x : expr (ℤ * ℤ * ℤ)%etype =>
    Base (#(fancy_addc log2wordmax imm)%expr @ x)%expr_pat
| fancy_sub log2wordmax imm =>
    fun x : expr (ℤ * ℤ)%etype =>
    Base (#(fancy_sub log2wordmax imm)%expr @ x)%expr_pat
| fancy_subb log2wordmax imm =>
    fun x : expr (ℤ * ℤ * ℤ)%etype =>
    Base (#(fancy_subb log2wordmax imm)%expr @ x)%expr_pat
| fancy_mulll log2wordmax =>
    fun x : expr (ℤ * ℤ)%etype =>
    Base (#(fancy_mulll log2wordmax)%expr @ x)%expr_pat
| fancy_mullh log2wordmax =>
    fun x : expr (ℤ * ℤ)%etype =>
    Base (#(fancy_mullh log2wordmax)%expr @ x)%expr_pat
| fancy_mulhl log2wordmax =>
    fun x : expr (ℤ * ℤ)%etype =>
    Base (#(fancy_mulhl log2wordmax)%expr @ x)%expr_pat
| fancy_mulhh log2wordmax =>
    fun x : expr (ℤ * ℤ)%etype =>
    Base (#(fancy_mulhh log2wordmax)%expr @ x)%expr_pat
| fancy_rshi log2wordmax x =>
    fun x0 : expr (ℤ * ℤ)%etype =>
    Base (#(fancy_rshi log2wordmax x)%expr @ x0)%expr_pat
| fancy_selc =>
    fun x : expr (ℤ * ℤ * ℤ)%etype => Base (#(fancy_selc)%expr @ x)%expr_pat
| fancy_selm log2wordmax =>
    fun x : expr (ℤ * ℤ * ℤ)%etype =>
    Base (#(fancy_selm log2wordmax)%expr @ x)%expr_pat
| fancy_sell =>
    fun x : expr (ℤ * ℤ * ℤ)%etype => Base (#(fancy_sell)%expr @ x)%expr_pat
| fancy_addm =>
    fun x : expr (ℤ * ℤ * ℤ)%etype => Base (#(fancy_addm)%expr @ x)%expr_pat
end
     : Compile.value' true t