nbe_rewrite_head = 
match idc in (ident t) return (Compile.value' true t) with
| @ident.Literal t v =>
    match
      t as t0
      return
        (base.base_interp t0 ->
         UnderLets.UnderLets base.type ident var
           (defaults.expr (type.base t0)))
    with
    | base.type.unit => fun v0 : unit => UnderLets.Base ##(v0)%expr
    | base.type.Z => fun v0 : Z => UnderLets.Base ##(v0)%expr
    | base.type.bool => fun v0 : bool => UnderLets.Base ##(v0)%expr
    | base.type.nat => fun v0 : nat => UnderLets.Base ##(v0)%expr
    end v
| ident.Nat_succ =>
    fun x : defaults.expr (type.base base.type.nat) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option nat) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun _ : Z => None
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun v0 : nat => Some v0
              end v
          | _ => None
          end
        with
        | Some args => UnderLets.Base ##(Nat.succ args)%expr
        | None => UnderLets.Base (#(ident.Nat_succ)%expr @ x)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.Nat_succ)%expr @ x)%expr_pat
    end
| ident.Nat_pred =>
    fun x : defaults.expr (type.base base.type.nat) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option nat) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun _ : Z => None
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun v0 : nat => Some v0
              end v
          | _ => None
          end
        with
        | Some args => UnderLets.Base ##(Nat.pred args)%expr
        | None => UnderLets.Base (#(ident.Nat_pred)%expr @ x)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.Nat_pred)%expr @ x)%expr_pat
    end
| ident.Nat_max =>
    fun x x0 : defaults.expr (type.base base.type.nat) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option nat) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun _ : Z => None
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun v0 : nat => Some v0
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option nat)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun _ : Z => None
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun v0 : nat => Some v0
                      end v
                  | _ => None
                  end
                with
                | Some args0 => UnderLets.Base ##(Nat.max args args0)%expr
                | None =>
                    UnderLets.Base (#(ident.Nat_max)%expr @ x @ x0)%expr_pat
                end
            | _ => UnderLets.Base (#(ident.Nat_max)%expr @ x @ x0)%expr_pat
            end
        | None => UnderLets.Base (#(ident.Nat_max)%expr @ x @ x0)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.Nat_max)%expr @ x @ x0)%expr_pat
    end
| ident.Nat_mul =>
    fun x x0 : defaults.expr (type.base base.type.nat) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option nat) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun _ : Z => None
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun v0 : nat => Some v0
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option nat)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun _ : Z => None
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun v0 : nat => Some v0
                      end v
                  | _ => None
                  end
                with
                | Some args0 => UnderLets.Base ##((args * args0)%nat)%expr
                | None =>
                    UnderLets.Base (#(ident.Nat_mul)%expr @ x @ x0)%expr_pat
                end
            | _ => UnderLets.Base (#(ident.Nat_mul)%expr @ x @ x0)%expr_pat
            end
        | None => UnderLets.Base (#(ident.Nat_mul)%expr @ x @ x0)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.Nat_mul)%expr @ x @ x0)%expr_pat
    end
| ident.Nat_add =>
    fun x x0 : defaults.expr (type.base base.type.nat) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option nat) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun _ : Z => None
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun v0 : nat => Some v0
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option nat)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun _ : Z => None
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun v0 : nat => Some v0
                      end v
                  | _ => None
                  end
                with
                | Some args0 => UnderLets.Base ##((args + args0)%nat)%expr
                | None =>
                    UnderLets.Base (#(ident.Nat_add)%expr @ x @ x0)%expr_pat
                end
            | _ => UnderLets.Base (#(ident.Nat_add)%expr @ x @ x0)%expr_pat
            end
        | None => UnderLets.Base (#(ident.Nat_add)%expr @ x @ x0)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.Nat_add)%expr @ x @ x0)%expr_pat
    end
| ident.Nat_sub =>
    fun x x0 : defaults.expr (type.base base.type.nat) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option nat) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun _ : Z => None
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun v0 : nat => Some v0
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option nat)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun _ : Z => None
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun v0 : nat => Some v0
                      end v
                  | _ => None
                  end
                with
                | Some args0 => UnderLets.Base ##((args - args0)%nat)%expr
                | None =>
                    UnderLets.Base (#(ident.Nat_sub)%expr @ x @ x0)%expr_pat
                end
            | _ => UnderLets.Base (#(ident.Nat_sub)%expr @ x @ x0)%expr_pat
            end
        | None => UnderLets.Base (#(ident.Nat_sub)%expr @ x @ x0)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.Nat_sub)%expr @ x @ x0)%expr_pat
    end
| @ident.nil t => UnderLets.Base []%expr_pat
| @ident.cons t =>
    fun (x : defaults.expr (type.base t))
      (x0 : defaults.expr (type.base (base.type.list t))) =>
    UnderLets.Base (x :: x0)%expr_pat
| @ident.pair A B =>
    fun (x : defaults.expr (type.base A)) (x0 : defaults.expr (type.base B))
    => UnderLets.Base (x, x0)%expr_pat
| @ident.fst A B =>
    fun x : defaults.expr (type.base (A * B)%etype) =>
    match x with
    | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ #(idc)%expr_pat x1) x0 =>
        match
          match idc with
          | @ident.pair A0 B0 => Some (A0, B0)
          | _ => None
          end
        with
        | Some _ =>
            match
              s0 as t2
              return
                (Compile.value' false t2 ->
                 UnderLets.UnderLets base.type ident var
                   (defaults.expr (type.base A)))
            with
            | type.base t2 =>
                fun v : defaults.expr (type.base t2) =>
                match
                  s as t3
                  return
                    (Compile.value' false t3 ->
                     UnderLets.UnderLets base.type ident var
                       (defaults.expr (type.base A)))
                with
                | type.base t3 =>
                    fun _ : defaults.expr (type.base t3) =>
                    base.try_make_transport_cps
                      (fun t0 : base.type => defaults.expr (type.base t0)) t2
                      A
                      (UnderLets.UnderLets base.type ident var
                         (defaults.expr (type.base A)))
                      (fun
                         a : option
                               (defaults.expr (type.base t2) ->
                                defaults.expr (type.base A)) =>
                       match a with
                       | Some x' => UnderLets.Base (x' v)
                       | None =>
                           UnderLets.Base (#(ident.fst)%expr @ x)%expr_pat
                       end)
                | (s1 -> d1)%ptype =>
                    fun _ : Compile.value' false s1 -> Compile.value' true d1
                    => UnderLets.Base (#(ident.fst)%expr @ x)%expr_pat
                end (Compile.reflect x0)
            | (s1 -> d1)%ptype =>
                fun _ : Compile.value' false s1 -> Compile.value' true d1 =>
                UnderLets.Base (#(ident.fst)%expr @ x)%expr_pat
            end (Compile.reflect x1)
        | None => UnderLets.Base (#(ident.fst)%expr @ x)%expr_pat
        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 _ _ _ _ _ _ _) _) _ =>
        UnderLets.Base (#(ident.fst)%expr @ x)%expr_pat
    | @expr.App _ _ _ s _ #(_)%expr_pat _ | @expr.App _ _ _ s _ ($_)%expr _ |
      @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _
      (@expr.LetIn _ _ _ _ _ _ _) _ =>
        UnderLets.Base (#(ident.fst)%expr @ x)%expr_pat
    | _ => UnderLets.Base (#(ident.fst)%expr @ x)%expr_pat
    end
| @ident.snd A B =>
    fun x : defaults.expr (type.base (A * B)%etype) =>
    match x with
    | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ #(idc)%expr_pat x1) x0 =>
        match
          match idc with
          | @ident.pair A0 B0 => Some (A0, B0)
          | _ => None
          end
        with
        | Some _ =>
            match
              s0 as t2
              return
                (Compile.value' false t2 ->
                 UnderLets.UnderLets base.type ident var
                   (defaults.expr (type.base B)))
            with
            | type.base t2 =>
                fun _ : defaults.expr (type.base t2) =>
                match
                  s as t3
                  return
                    (Compile.value' false t3 ->
                     UnderLets.UnderLets base.type ident var
                       (defaults.expr (type.base B)))
                with
                | type.base t3 =>
                    fun v0 : defaults.expr (type.base t3) =>
                    base.try_make_transport_cps
                      (fun t0 : base.type => defaults.expr (type.base t0)) t3
                      B
                      (UnderLets.UnderLets base.type ident var
                         (defaults.expr (type.base B)))
                      (fun
                         a : option
                               (defaults.expr (type.base t3) ->
                                defaults.expr (type.base B)) =>
                       match a with
                       | Some x' => UnderLets.Base (x' v0)
                       | None =>
                           UnderLets.Base (#(ident.snd)%expr @ x)%expr_pat
                       end)
                | (s1 -> d1)%ptype =>
                    fun _ : Compile.value' false s1 -> Compile.value' true d1
                    => UnderLets.Base (#(ident.snd)%expr @ x)%expr_pat
                end (Compile.reflect x0)
            | (s1 -> d1)%ptype =>
                fun _ : Compile.value' false s1 -> Compile.value' true d1 =>
                UnderLets.Base (#(ident.snd)%expr @ x)%expr_pat
            end (Compile.reflect x1)
        | None => UnderLets.Base (#(ident.snd)%expr @ x)%expr_pat
        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 _ _ _ _ _ _ _) _) _ =>
        UnderLets.Base (#(ident.snd)%expr @ x)%expr_pat
    | @expr.App _ _ _ s _ #(_)%expr_pat _ | @expr.App _ _ _ s _ ($_)%expr _ |
      @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _
      (@expr.LetIn _ _ _ _ _ _ _) _ =>
        UnderLets.Base (#(ident.snd)%expr @ x)%expr_pat
    | _ => UnderLets.Base (#(ident.snd)%expr @ x)%expr_pat
    end
| @ident.prod_rect A B T =>
    fun
      (x : defaults.expr (type.base A) ->
           defaults.expr (type.base B) ->
           UnderLets.UnderLets base.type ident var
             (defaults.expr (type.base T)))
      (x0 : defaults.expr (type.base (A * B)%etype)) =>
    match x0 with
    | @expr.App _ _ _ s _ #(_)%expr_pat _ | @expr.App _ _ _ s _ ($_)%expr _ |
      @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ =>
        UnderLets.Base
          (#(ident.prod_rect)%expr @
           (λ (x2 : var (type.base A))(x3 : var (type.base B)),
            UnderLets.to_expr (x ($x2) ($x3)))%expr @ x0)%expr_pat
    | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ #(idc)%expr_pat x2) x1 =>
        match
          match idc with
          | @ident.pair A0 B0 => Some (A0, B0)
          | _ => None
          end
        with
        | Some _ =>
            match
              s0 as t2
              return
                (Compile.value' false t2 ->
                 UnderLets.UnderLets base.type ident var
                   (defaults.expr (type.base T)))
            with
            | type.base t2 =>
                fun v : defaults.expr (type.base t2) =>
                match
                  s as t3
                  return
                    (Compile.value' false t3 ->
                     UnderLets.UnderLets base.type ident var
                       (defaults.expr (type.base T)))
                with
                | type.base t3 =>
                    fun v0 : defaults.expr (type.base t3) =>
                    Compile.castbe v
                      (UnderLets.UnderLets base.type ident var
                         (defaults.expr (type.base T)))
                      (fun x3 : option (defaults.expr (type.base A)) =>
                       match x3 with
                       | Some x4 =>
                           Compile.castbe v0
                             (UnderLets.UnderLets base.type ident var
                                (defaults.expr (type.base T)))
                             (fun y : option (defaults.expr (type.base B)) =>
                              match y with
                              | Some y0 =>
                                  (fv <-- (e <-- x x4 y0;
                                           UnderLets.Base
                                             {|
                                             anyexpr_ty := T;
                                             unwrap := e |});
                                   base.try_make_transport_cps
                                     (fun t0 : base.type =>
                                      defaults.expr (type.base t0))
                                     (let (anyexpr_ty, _) := fv in anyexpr_ty)
                                     T
                                     (UnderLets.UnderLets base.type ident var
                                        (defaults.expr (type.base T)))
                                     (fun
                                        a : option
                                              (defaults.expr
                                                 (type.base
                                                    (let (anyexpr_ty, _) :=
                                                       fv in
                                                     anyexpr_ty)) ->
                                               defaults.expr (type.base T))
                                      =>
                                      match a with
                                      | Some x' =>
                                          UnderLets.Base
                                            (x'
                                               (let
                                                  (anyexpr_ty, unwrap) as a0
                                                   return
                                                     (defaults.expr
                                                        (type.base
                                                           (let
                                                              (anyexpr_ty,
                                                               _) := a0 in
                                                            anyexpr_ty))) :=
                                                  fv in
                                                unwrap))
                                      | None =>
                                          UnderLets.Base
                                            (#(ident.prod_rect)%expr @
                                             (λ (x5 : var (type.base A))
                                              (x6 : var (type.base B)),
                                              UnderLets.to_expr
                                                (x ($x5) ($x6)))%expr @ x0)%expr_pat
                                      end))%under_lets
                              | None =>
                                  UnderLets.Base
                                    (#(ident.prod_rect)%expr @
                                     (λ (x5 : var (type.base A))(x6 : 
                                                                 var
                                                                   (type.base
                                                                    B)),
                                      UnderLets.to_expr (x ($x5) ($x6)))%expr @
                                     x0)%expr_pat
                              end)
                       | None =>
                           UnderLets.Base
                             (#(ident.prod_rect)%expr @
                              (λ (x4 : var (type.base A))(x5 : var
                                                                 (type.base B)),
                               UnderLets.to_expr (x ($x4) ($x5)))%expr @ x0)%expr_pat
                       end)
                | (s1 -> d1)%ptype =>
                    fun _ : Compile.value' false s1 -> Compile.value' true d1
                    =>
                    UnderLets.Base
                      (#(ident.prod_rect)%expr @
                       (λ (x3 : var (type.base A))(x4 : var (type.base B)),
                        UnderLets.to_expr (x ($x3) ($x4)))%expr @ x0)%expr_pat
                end (Compile.reflect x1)
            | (s1 -> d1)%ptype =>
                fun _ : Compile.value' false s1 -> Compile.value' true d1 =>
                UnderLets.Base
                  (#(ident.prod_rect)%expr @
                   (λ (x3 : var (type.base A))(x4 : var (type.base B)),
                    UnderLets.to_expr (x ($x3) ($x4)))%expr @ x0)%expr_pat
            end (Compile.reflect x2)
        | None =>
            UnderLets.Base
              (#(ident.prod_rect)%expr @
               (λ (x3 : var (type.base A))(x4 : var (type.base B)),
                UnderLets.to_expr (x ($x3) ($x4)))%expr @ x0)%expr_pat
        end
    | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App _
      _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ =>
        UnderLets.Base
          (#(ident.prod_rect)%expr @
           (λ (x3 : var (type.base A))(x4 : var (type.base B)),
            UnderLets.to_expr (x ($x3) ($x4)))%expr @ x0)%expr_pat
    | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (_ @ _)%expr_pat _) _ |
      @expr.App _ _ _ s _
      (@expr.App _ _ _ s0 _ (@expr.LetIn _ _ _ _ _ _ _) _) _ =>
        UnderLets.Base
          (#(ident.prod_rect)%expr @
           (λ (x4 : var (type.base A))(x5 : var (type.base B)),
            UnderLets.to_expr (x ($x4) ($x5)))%expr @ x0)%expr_pat
    | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ =>
        UnderLets.Base
          (#(ident.prod_rect)%expr @
           (λ (x3 : var (type.base A))(x4 : var (type.base B)),
            UnderLets.to_expr (x ($x3) ($x4)))%expr @ x0)%expr_pat
    | @expr.LetIn _ _ _ _ _ _ _ =>
        UnderLets.Base
          (#(ident.prod_rect)%expr @
           (λ (x2 : var (type.base A))(x3 : var (type.base B)),
            UnderLets.to_expr (x ($x2) ($x3)))%expr @ x0)%expr_pat
    | _ =>
        UnderLets.Base
          (#(ident.prod_rect)%expr @
           (λ (x1 : var (type.base A))(x2 : var (type.base B)),
            UnderLets.to_expr (x ($x1) ($x2)))%expr @ x0)%expr_pat
    end
| @ident.bool_rect T =>
    fun
      (x
       x0 : defaults.expr (type.base base.type.unit) ->
            UnderLets.UnderLets base.type ident var
              (defaults.expr (type.base T)))
      (x1 : defaults.expr (type.base base.type.bool)) =>
    match x1 with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option bool) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun _ : Z => None
              | base.type.bool => fun v0 : bool => Some v0
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args =>
            (fv <-- (e <-- (if args as b
                             return
                               (UnderLets.UnderLets base.type ident var
                                  (defaults.expr
                                     (type.base (if b then T else T))))
                            then x ##(tt)%expr
                            else x0 ##(tt)%expr);
                     UnderLets.Base
                       {| anyexpr_ty := if args then T else T; unwrap := e |});
             base.try_make_transport_cps
               (fun t0 : base.type => defaults.expr (type.base t0))
               (let (anyexpr_ty, _) := fv in anyexpr_ty) T
               (UnderLets.UnderLets base.type ident var
                  (defaults.expr (type.base T)))
               (fun
                  a : option
                        (defaults.expr
                           (type.base
                              (let (anyexpr_ty, _) := fv in anyexpr_ty)) ->
                         defaults.expr (type.base T)) =>
                match a with
                | Some x' =>
                    UnderLets.Base
                      (x'
                         (let
                            (anyexpr_ty, unwrap) as a0
                             return
                               (defaults.expr
                                  (type.base
                                     (let (anyexpr_ty, _) := a0 in anyexpr_ty))) :=
                            fv in
                          unwrap))
                | None =>
                    UnderLets.Base
                      (#(ident.bool_rect)%expr @
                       (λ x2 : var (type.base base.type.unit),
                        UnderLets.to_expr (x ($x2)))%expr @
                       (λ x2 : var (type.base base.type.unit),
                        UnderLets.to_expr (x0 ($x2)))%expr @ x1)%expr_pat
                end))%under_lets
        | None =>
            UnderLets.Base
              (#(ident.bool_rect)%expr @
               (λ x2 : var (type.base base.type.unit),
                UnderLets.to_expr (x ($x2)))%expr @
               (λ x2 : var (type.base base.type.unit),
                UnderLets.to_expr (x0 ($x2)))%expr @ x1)%expr_pat
        end
    | ($_)%expr | @expr.Abs _ _ _ _ _ _ =>
        UnderLets.Base
          (#(ident.bool_rect)%expr @
           (λ x2 : var (type.base base.type.unit),
            UnderLets.to_expr (x ($x2)))%expr @
           (λ x2 : var (type.base base.type.unit),
            UnderLets.to_expr (x0 ($x2)))%expr @ x1)%expr_pat
    | _ =>
        UnderLets.Base
          (#(ident.bool_rect)%expr @
           (λ x3 : var (type.base base.type.unit),
            UnderLets.to_expr (x ($x3)))%expr @
           (λ x3 : var (type.base base.type.unit),
            UnderLets.to_expr (x0 ($x3)))%expr @ x1)%expr_pat
    end
| @ident.nat_rect P =>
    fun
      (x : defaults.expr (type.base base.type.unit) ->
           UnderLets.UnderLets base.type ident var
             (defaults.expr (type.base P)))
      (x0 : defaults.expr (type.base base.type.nat) ->
            defaults.expr (type.base P) ->
            UnderLets.UnderLets base.type ident var
              (defaults.expr (type.base P)))
      (x1 : defaults.expr (type.base base.type.nat)) =>
    match x1 with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option nat) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun _ : Z => None
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun v0 : nat => Some v0
              end v
          | _ => None
          end
        with
        | Some args =>
            Compile.castv x0
              (UnderLets.UnderLets base.type ident var
                 (defaults.expr (type.base P)))
              (fun
                 S_case : option
                            (defaults.expr (type.base base.type.nat) ->
                             defaults.expr (type.base P) ->
                             UnderLets.UnderLets base.type ident var
                               (defaults.expr (type.base P))) =>
               match S_case with
               | Some S_case0 =>
                   (fv <-- (e <-- nat_rect
                                    (fun _ : nat =>
                                     UnderLets.UnderLets base.type ident var
                                       (defaults.expr (type.base P)))
                                    (x ##(tt)%expr)
                                    (fun (n' : nat)
                                       (rec : UnderLets.UnderLets base.type
                                                ident var
                                                (defaults.expr (type.base P)))
                                     => rec0 <-- rec;
                                        S_case0 ##(n')%expr rec0) args;
                            UnderLets.Base {| anyexpr_ty := P; unwrap := e |});
                    base.try_make_transport_cps
                      (fun t0 : base.type => defaults.expr (type.base t0))
                      (let (anyexpr_ty, _) := fv in anyexpr_ty) P
                      (UnderLets.UnderLets base.type ident var
                         (defaults.expr (type.base P)))
                      (fun
                         a : option
                               (defaults.expr
                                  (type.base
                                     (let (anyexpr_ty, _) := fv in anyexpr_ty)) ->
                                defaults.expr (type.base P)) =>
                       match a with
                       | Some x' =>
                           UnderLets.Base
                             (x'
                                (let
                                   (anyexpr_ty, unwrap) as a0
                                    return
                                      (defaults.expr
                                         (type.base
                                            (let (anyexpr_ty, _) := a0 in
                                             anyexpr_ty))) := fv in
                                 unwrap))
                       | None =>
                           UnderLets.Base
                             (#(ident.nat_rect)%expr @
                              (λ x2 : var (type.base base.type.unit),
                               UnderLets.to_expr (x ($x2)))%expr @
                              (λ (x2 : var (type.base base.type.nat))
                               (x3 : var (type.base P)),
                               UnderLets.to_expr (x0 ($x2) ($x3)))%expr @ x1)%expr_pat
                       end))%under_lets
               | None =>
                   UnderLets.Base
                     (#(ident.nat_rect)%expr @
                      (λ x2 : var (type.base base.type.unit),
                       UnderLets.to_expr (x ($x2)))%expr @
                      (λ (x2 : var (type.base base.type.nat))(x3 : var
                                                                    (type.base
                                                                    P)),
                       UnderLets.to_expr (x0 ($x2) ($x3)))%expr @ x1)%expr_pat
               end)
        | None =>
            UnderLets.Base
              (#(ident.nat_rect)%expr @
               (λ x2 : var (type.base base.type.unit),
                UnderLets.to_expr (x ($x2)))%expr @
               (λ (x2 : var (type.base base.type.nat))(x3 : var (type.base P)),
                UnderLets.to_expr (x0 ($x2) ($x3)))%expr @ x1)%expr_pat
        end
    | ($_)%expr | @expr.Abs _ _ _ _ _ _ =>
        UnderLets.Base
          (#(ident.nat_rect)%expr @
           (λ x2 : var (type.base base.type.unit),
            UnderLets.to_expr (x ($x2)))%expr @
           (λ (x2 : var (type.base base.type.nat))(x3 : var (type.base P)),
            UnderLets.to_expr (x0 ($x2) ($x3)))%expr @ x1)%expr_pat
    | _ =>
        UnderLets.Base
          (#(ident.nat_rect)%expr @
           (λ x3 : var (type.base base.type.unit),
            UnderLets.to_expr (x ($x3)))%expr @
           (λ (x3 : var (type.base base.type.nat))(x4 : var (type.base P)),
            UnderLets.to_expr (x0 ($x3) ($x4)))%expr @ x1)%expr_pat
    end
| @ident.nat_rect_arrow P Q =>
    fun
      (x : defaults.expr (type.base P) ->
           UnderLets.UnderLets base.type ident var
             (defaults.expr (type.base Q)))
      (x0 : defaults.expr (type.base base.type.nat) ->
            (defaults.expr (type.base P) ->
             UnderLets.UnderLets base.type ident var
               (defaults.expr (type.base Q))) ->
            defaults.expr (type.base P) ->
            UnderLets.UnderLets base.type ident var
              (defaults.expr (type.base Q)))
      (x1 : defaults.expr (type.base base.type.nat))
      (x2 : defaults.expr (type.base P)) =>
    match x1 with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option nat) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun _ : Z => None
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun v0 : nat => Some v0
              end v
          | _ => None
          end
        with
        | Some args =>
            Compile.castv x0
              (UnderLets.UnderLets base.type ident var
                 (defaults.expr (type.base Q)))
              (fun
                 S_case : option
                            (defaults.expr (type.base base.type.nat) ->
                             (defaults.expr (type.base P) ->
                              UnderLets.UnderLets base.type ident var
                                (defaults.expr (type.base Q))) ->
                             defaults.expr (type.base P) ->
                             UnderLets.UnderLets base.type ident var
                               (defaults.expr (type.base Q))) =>
               match S_case with
               | Some S_case0 =>
                   Compile.castbe x2
                     (UnderLets.UnderLets base.type ident var
                        (defaults.expr (type.base Q)))
                     (fun v : option (defaults.expr (type.base P)) =>
                      match v with
                      | Some v0 =>
                          (fv <-- (e <-- nat_rect
                                           (fun _ : nat =>
                                            defaults.expr (type.base P) ->
                                            UnderLets.UnderLets base.type
                                              ident var
                                              (defaults.expr (type.base Q)))
                                           x
                                           (fun (n' : nat)
                                              (rec : defaults.expr
                                                       (type.base P) ->
                                                     UnderLets.UnderLets
                                                       base.type ident var
                                                       (defaults.expr
                                                          (type.base Q)))
                                              (v1 : defaults.expr
                                                      (type.base P)) =>
                                            S_case0 ##(n')%expr rec v1) args
                                           v0;
                                   UnderLets.Base
                                     {| anyexpr_ty := Q; unwrap := e |});
                           base.try_make_transport_cps
                             (fun t0 : base.type =>
                              defaults.expr (type.base t0))
                             (let (anyexpr_ty, _) := fv in anyexpr_ty) Q
                             (UnderLets.UnderLets base.type ident var
                                (defaults.expr (type.base Q)))
                             (fun
                                a : option
                                      (defaults.expr
                                         (type.base
                                            (let (anyexpr_ty, _) := fv in
                                             anyexpr_ty)) ->
                                       defaults.expr (type.base Q)) =>
                              match a with
                              | Some x' =>
                                  UnderLets.Base
                                    (x'
                                       (let
                                          (anyexpr_ty, unwrap) as a0
                                           return
                                             (defaults.expr
                                                (type.base
                                                   (let (anyexpr_ty, _) :=
                                                      a0 in
                                                    anyexpr_ty))) := fv in
                                        unwrap))
                              | None =>
                                  UnderLets.Base
                                    (#(ident.nat_rect_arrow)%expr @
                                     (λ x3 : var (type.base P),
                                      UnderLets.to_expr (x ($x3)))%expr @
                                     (λ (x3 : var (type.base base.type.nat))
                                      (x4 : var
                                              (type.base P -> type.base Q)%ptype)
                                      (x5 : var (type.base P)),
                                      UnderLets.to_expr
                                        (x0 ($x3)
                                           (fun
                                              x6 : defaults.expr
                                                     (type.base P) =>
                                            UnderLets.Base
                                              ($x4 @ x6)%expr_pat) ($x5)))%expr @
                                     x1 @ x2)%expr_pat
                              end))%under_lets
                      | None =>
                          UnderLets.Base
                            (#(ident.nat_rect_arrow)%expr @
                             (λ x3 : var (type.base P),
                              UnderLets.to_expr (x ($x3)))%expr @
                             (λ (x3 : var (type.base base.type.nat))(x4 : 
                                                                    var
                                                                    (type.base
                                                                    P ->
                                                                    type.base
                                                                    Q)%ptype)
                              (x5 : var (type.base P)),
                              UnderLets.to_expr
                                (x0 ($x3)
                                   (fun x6 : defaults.expr (type.base P) =>
                                    UnderLets.Base ($x4 @ x6)%expr_pat) 
                                   ($x5)))%expr @ x1 @ x2)%expr_pat
                      end)
               | None =>
                   UnderLets.Base
                     (#(ident.nat_rect_arrow)%expr @
                      (λ x3 : var (type.base P),
                       UnderLets.to_expr (x ($x3)))%expr @
                      (λ (x3 : var (type.base base.type.nat))(x4 : var
                                                                    (type.base
                                                                    P ->
                                                                    type.base
                                                                    Q)%ptype)
                       (x5 : var (type.base P)),
                       UnderLets.to_expr
                         (x0 ($x3)
                            (fun x6 : defaults.expr (type.base P) =>
                             UnderLets.Base ($x4 @ x6)%expr_pat) ($x5)))%expr @
                      x1 @ x2)%expr_pat
               end)
        | None =>
            UnderLets.Base
              (#(ident.nat_rect_arrow)%expr @
               (λ x3 : var (type.base P),
                UnderLets.to_expr (x ($x3)))%expr @
               (λ (x3 : var (type.base base.type.nat))(x4 : var
                                                              (type.base P ->
                                                               type.base Q)%ptype)
                (x5 : var (type.base P)),
                UnderLets.to_expr
                  (x0 ($x3)
                     (fun x6 : defaults.expr (type.base P) =>
                      UnderLets.Base ($x4 @ x6)%expr_pat) ($x5)))%expr @ x1 @
               x2)%expr_pat
        end
    | ($_)%expr | @expr.Abs _ _ _ _ _ _ =>
        UnderLets.Base
          (#(ident.nat_rect_arrow)%expr @
           (λ x3 : var (type.base P),
            UnderLets.to_expr (x ($x3)))%expr @
           (λ (x3 : var (type.base base.type.nat))(x4 : var
                                                          (type.base P ->
                                                           type.base Q)%ptype)
            (x5 : var (type.base P)),
            UnderLets.to_expr
              (x0 ($x3)
                 (fun x6 : defaults.expr (type.base P) =>
                  UnderLets.Base ($x4 @ x6)%expr_pat) ($x5)))%expr @ x1 @ x2)%expr_pat
    | _ =>
        UnderLets.Base
          (#(ident.nat_rect_arrow)%expr @
           (λ x4 : var (type.base P),
            UnderLets.to_expr (x ($x4)))%expr @
           (λ (x4 : var (type.base base.type.nat))(x5 : var
                                                          (type.base P ->
                                                           type.base Q)%ptype)
            (x6 : var (type.base P)),
            UnderLets.to_expr
              (x0 ($x4)
                 (fun x7 : defaults.expr (type.base P) =>
                  UnderLets.Base ($x5 @ x7)%expr_pat) ($x6)))%expr @ x1 @ x2)%expr_pat
    end
| @ident.list_rect A P =>
    fun
      (x : defaults.expr (type.base base.type.unit) ->
           UnderLets.UnderLets base.type ident var
             (defaults.expr (type.base P)))
      (x0 : defaults.expr (type.base A) ->
            defaults.expr (type.base (base.type.list A)) ->
            defaults.expr (type.base P) ->
            UnderLets.UnderLets base.type ident var
              (defaults.expr (type.base P)))
      (x1 : defaults.expr (type.base (base.type.list A))) =>
    Compile.castv x0
      (UnderLets.UnderLets base.type ident var (defaults.expr (type.base P)))
      (fun
         Pcons : option
                   (defaults.expr (type.base A) ->
                    defaults.expr (type.base (base.type.list A)) ->
                    defaults.expr (type.base P) ->
                    UnderLets.UnderLets base.type ident var
                      (defaults.expr (type.base P))) =>
       match Pcons with
       | Some Pcons0 =>
           reflect_list_cps x1
             (fun ls : option (list (defaults.expr (type.base A))) =>
              match ls with
              | Some ls0 =>
                  (fv <-- (e <-- list_rect
                                   (fun
                                      _ : list (defaults.expr (type.base A))
                                    =>
                                    UnderLets.UnderLets base.type ident var
                                      (defaults.expr (type.base P)))
                                   (x ##(tt)%expr)
                                   (fun (x2 : defaults.expr (type.base A))
                                      (xs : list
                                              (defaults.expr (type.base A)))
                                      (rec : UnderLets.UnderLets base.type
                                               ident var
                                               (defaults.expr (type.base P)))
                                    =>
                                    rec' <-- rec;
                                    Pcons0 x2 (reify_list xs) rec') ls0;
                           UnderLets.Base {| anyexpr_ty := P; unwrap := e |});
                   base.try_make_transport_cps
                     (fun t : base.type => defaults.expr (type.base t))
                     (let (anyexpr_ty, _) := fv in anyexpr_ty) P
                     (UnderLets.UnderLets base.type ident var
                        (defaults.expr (type.base P)))
                     (fun
                        a : option
                              (defaults.expr
                                 (type.base
                                    (let (anyexpr_ty, _) := fv in anyexpr_ty)) ->
                               defaults.expr (type.base P)) =>
                      match a with
                      | Some x' =>
                          UnderLets.Base
                            (x'
                               (let
                                  (anyexpr_ty, unwrap) as a0
                                   return
                                     (defaults.expr
                                        (type.base
                                           (let (anyexpr_ty, _) := a0 in
                                            anyexpr_ty))) := fv in
                                unwrap))
                      | None =>
                          UnderLets.Base
                            (#(ident.list_rect)%expr @
                             (λ x2 : var (type.base base.type.unit),
                              UnderLets.to_expr (x ($x2)))%expr @
                             (λ (x2 : var (type.base A))(x3 : var
                                                                (type.base
                                                                   (base.type.list
                                                                    A)))
                              (x4 : var (type.base P)),
                              UnderLets.to_expr (x0 ($x2) ($x3) ($x4)))%expr @
                             x1)%expr_pat
                      end))%under_lets
              | None =>
                  UnderLets.Base
                    (#(ident.list_rect)%expr @
                     (λ x2 : var (type.base base.type.unit),
                      UnderLets.to_expr (x ($x2)))%expr @
                     (λ (x2 : var (type.base A))(x3 : var
                                                        (type.base
                                                           (base.type.list A)))
                      (x4 : var (type.base P)),
                      UnderLets.to_expr (x0 ($x2) ($x3) ($x4)))%expr @ x1)%expr_pat
              end)
       | None =>
           UnderLets.Base
             (#(ident.list_rect)%expr @
              (λ x2 : var (type.base base.type.unit),
               UnderLets.to_expr (x ($x2)))%expr @
              (λ (x2 : var (type.base A))(x3 : var
                                                 (type.base
                                                    (base.type.list A)))
               (x4 : var (type.base P)),
               UnderLets.to_expr (x0 ($x2) ($x3) ($x4)))%expr @ x1)%expr_pat
       end)
| @ident.list_case A P =>
    fun
      (x : defaults.expr (type.base base.type.unit) ->
           UnderLets.UnderLets base.type ident var
             (defaults.expr (type.base P)))
      (x0 : defaults.expr (type.base A) ->
            defaults.expr (type.base (base.type.list A)) ->
            UnderLets.UnderLets base.type ident var
              (defaults.expr (type.base P)))
      (x1 : defaults.expr (type.base (base.type.list A))) =>
    match x1 with
    | #(idc)%expr_pat =>
        match match idc with
              | @ident.nil t0 => Some t0
              | _ => None
              end with
        | Some _ =>
            (fv <-- (e <-- x ##(tt)%expr;
                     UnderLets.Base {| anyexpr_ty := P; unwrap := e |});
             base.try_make_transport_cps
               (fun t0 : base.type => defaults.expr (type.base t0))
               (let (anyexpr_ty, _) := fv in anyexpr_ty) P
               (UnderLets.UnderLets base.type ident var
                  (defaults.expr (type.base P)))
               (fun
                  a : option
                        (defaults.expr
                           (type.base
                              (let (anyexpr_ty, _) := fv in anyexpr_ty)) ->
                         defaults.expr (type.base P)) =>
                match a with
                | Some x' =>
                    UnderLets.Base
                      (x'
                         (let
                            (anyexpr_ty, unwrap) as a0
                             return
                               (defaults.expr
                                  (type.base
                                     (let (anyexpr_ty, _) := a0 in anyexpr_ty))) :=
                            fv in
                          unwrap))
                | None =>
                    UnderLets.Base
                      (#(ident.list_case)%expr @
                       (λ x2 : var (type.base base.type.unit),
                        UnderLets.to_expr (x ($x2)))%expr @
                       (λ (x2 : var (type.base A))(x3 : var
                                                          (type.base
                                                             (base.type.list
                                                                A))),
                        UnderLets.to_expr (x0 ($x2) ($x3)))%expr @ x1)%expr_pat
                end))%under_lets
        | None =>
            UnderLets.Base
              (#(ident.list_case)%expr @
               (λ x2 : var (type.base base.type.unit),
                UnderLets.to_expr (x ($x2)))%expr @
               (λ (x2 : var (type.base A))(x3 : var
                                                  (type.base
                                                     (base.type.list A))),
                UnderLets.to_expr (x0 ($x2) ($x3)))%expr @ x1)%expr_pat
        end
    | @expr.App _ _ _ s _ #(_)%expr_pat _ | @expr.App _ _ _ s _ ($_)%expr _ |
      @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ =>
        UnderLets.Base
          (#(ident.list_case)%expr @
           (λ x3 : var (type.base base.type.unit),
            UnderLets.to_expr (x ($x3)))%expr @
           (λ (x3 : var (type.base A))(x4 : var
                                              (type.base (base.type.list A))),
            UnderLets.to_expr (x0 ($x3) ($x4)))%expr @ x1)%expr_pat
    | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ #(idc)%expr_pat x3) x2 =>
        match match idc with
              | @ident.cons t0 => Some t0
              | _ => None
              end with
        | Some _ =>
            match
              s0 as t2
              return
                (Compile.value' false t2 ->
                 UnderLets.UnderLets base.type ident var
                   (defaults.expr (type.base P)))
            with
            | type.base t2 =>
                fun v : defaults.expr (type.base t2) =>
                match
                  s as t3
                  return
                    (Compile.value' false t3 ->
                     UnderLets.UnderLets base.type ident var
                       (defaults.expr (type.base P)))
                with
                | type.base t3 =>
                    fun v0 : defaults.expr (type.base t3) =>
                    Compile.castbe v
                      (UnderLets.UnderLets base.type ident var
                         (defaults.expr (type.base P)))
                      (fun x4 : option (defaults.expr (type.base A)) =>
                       match x4 with
                       | Some x5 =>
                           Compile.castbe v0
                             (UnderLets.UnderLets base.type ident var
                                (defaults.expr (type.base P)))
                             (fun
                                xs : option
                                       (defaults.expr
                                          (type.base (base.type.list A))) =>
                              match xs with
                              | Some xs0 =>
                                  (fv <-- (e <-- x0 x5 xs0;
                                           UnderLets.Base
                                             {|
                                             anyexpr_ty := P;
                                             unwrap := e |});
                                   base.try_make_transport_cps
                                     (fun t0 : base.type =>
                                      defaults.expr (type.base t0))
                                     (let (anyexpr_ty, _) := fv in anyexpr_ty)
                                     P
                                     (UnderLets.UnderLets base.type ident var
                                        (defaults.expr (type.base P)))
                                     (fun
                                        a : option
                                              (defaults.expr
                                                 (type.base
                                                    (let (anyexpr_ty, _) :=
                                                       fv in
                                                     anyexpr_ty)) ->
                                               defaults.expr (type.base P))
                                      =>
                                      match a with
                                      | Some x' =>
                                          UnderLets.Base
                                            (x'
                                               (let
                                                  (anyexpr_ty, unwrap) as a0
                                                   return
                                                     (defaults.expr
                                                        (type.base
                                                           (let
                                                              (anyexpr_ty,
                                                               _) := a0 in
                                                            anyexpr_ty))) :=
                                                  fv in
                                                unwrap))
                                      | None =>
                                          UnderLets.Base
                                            (#(ident.list_case)%expr @
                                             (λ x6 : var
                                                       (type.base
                                                          base.type.unit),
                                              UnderLets.to_expr (x ($x6)))%expr @
                                             (λ (x6 : var (type.base A))
                                              (x7 : var
                                                      (type.base
                                                         (base.type.list A))),
                                              UnderLets.to_expr
                                                (x0 ($x6) ($x7)))%expr @ x1)%expr_pat
                                      end))%under_lets
                              | None =>
                                  UnderLets.Base
                                    (#(ident.list_case)%expr @
                                     (λ x6 : var (type.base base.type.unit),
                                      UnderLets.to_expr (x ($x6)))%expr @
                                     (λ (x6 : var (type.base A))(x7 : 
                                                                 var
                                                                   (type.base
                                                                    (base.type.list
                                                                    A))),
                                      UnderLets.to_expr (x0 ($x6) ($x7)))%expr @
                                     x1)%expr_pat
                              end)
                       | None =>
                           UnderLets.Base
                             (#(ident.list_case)%expr @
                              (λ x5 : var (type.base base.type.unit),
                               UnderLets.to_expr (x ($x5)))%expr @
                              (λ (x5 : var (type.base A))(x6 : var
                                                                 (type.base
                                                                    (base.type.list
                                                                    A))),
                               UnderLets.to_expr (x0 ($x5) ($x6)))%expr @ x1)%expr_pat
                       end)
                | (s1 -> d1)%ptype =>
                    fun _ : Compile.value' false s1 -> Compile.value' true d1
                    =>
                    UnderLets.Base
                      (#(ident.list_case)%expr @
                       (λ x4 : var (type.base base.type.unit),
                        UnderLets.to_expr (x ($x4)))%expr @
                       (λ (x4 : var (type.base A))(x5 : var
                                                          (type.base
                                                             (base.type.list
                                                                A))),
                        UnderLets.to_expr (x0 ($x4) ($x5)))%expr @ x1)%expr_pat
                end (Compile.reflect x2)
            | (s1 -> d1)%ptype =>
                fun _ : Compile.value' false s1 -> Compile.value' true d1 =>
                UnderLets.Base
                  (#(ident.list_case)%expr @
                   (λ x4 : var (type.base base.type.unit),
                    UnderLets.to_expr (x ($x4)))%expr @
                   (λ (x4 : var (type.base A))(x5 : var
                                                      (type.base
                                                         (base.type.list A))),
                    UnderLets.to_expr (x0 ($x4) ($x5)))%expr @ x1)%expr_pat
            end (Compile.reflect x3)
        | None =>
            UnderLets.Base
              (#(ident.list_case)%expr @
               (λ x4 : var (type.base base.type.unit),
                UnderLets.to_expr (x ($x4)))%expr @
               (λ (x4 : var (type.base A))(x5 : var
                                                  (type.base
                                                     (base.type.list A))),
                UnderLets.to_expr (x0 ($x4) ($x5)))%expr @ x1)%expr_pat
        end
    | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App _
      _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ =>
        UnderLets.Base
          (#(ident.list_case)%expr @
           (λ x4 : var (type.base base.type.unit),
            UnderLets.to_expr (x ($x4)))%expr @
           (λ (x4 : var (type.base A))(x5 : var
                                              (type.base (base.type.list A))),
            UnderLets.to_expr (x0 ($x4) ($x5)))%expr @ x1)%expr_pat
    | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (_ @ _)%expr_pat _) _ |
      @expr.App _ _ _ s _
      (@expr.App _ _ _ s0 _ (@expr.LetIn _ _ _ _ _ _ _) _) _ =>
        UnderLets.Base
          (#(ident.list_case)%expr @
           (λ x5 : var (type.base base.type.unit),
            UnderLets.to_expr (x ($x5)))%expr @
           (λ (x5 : var (type.base A))(x6 : var
                                              (type.base (base.type.list A))),
            UnderLets.to_expr (x0 ($x5) ($x6)))%expr @ x1)%expr_pat
    | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ =>
        UnderLets.Base
          (#(ident.list_case)%expr @
           (λ x4 : var (type.base base.type.unit),
            UnderLets.to_expr (x ($x4)))%expr @
           (λ (x4 : var (type.base A))(x5 : var
                                              (type.base (base.type.list A))),
            UnderLets.to_expr (x0 ($x4) ($x5)))%expr @ x1)%expr_pat
    | @expr.LetIn _ _ _ _ _ _ _ =>
        UnderLets.Base
          (#(ident.list_case)%expr @
           (λ x3 : var (type.base base.type.unit),
            UnderLets.to_expr (x ($x3)))%expr @
           (λ (x3 : var (type.base A))(x4 : var
                                              (type.base (base.type.list A))),
            UnderLets.to_expr (x0 ($x3) ($x4)))%expr @ x1)%expr_pat
    | _ =>
        UnderLets.Base
          (#(ident.list_case)%expr @
           (λ x2 : var (type.base base.type.unit),
            UnderLets.to_expr (x ($x2)))%expr @
           (λ (x2 : var (type.base A))(x3 : var
                                              (type.base (base.type.list A))),
            UnderLets.to_expr (x0 ($x2) ($x3)))%expr @ x1)%expr_pat
    end
| @ident.List_length T =>
    fun x : defaults.expr (type.base (base.type.list T)) =>
    reflect_list_cps x
      (fun xs : option (list (defaults.expr (type.base T))) =>
       match xs with
       | Some xs0 => UnderLets.Base ##(length xs0)%expr
       | None => UnderLets.Base (#(ident.List_length)%expr @ x)%expr_pat
       end)
| ident.List_seq =>
    fun x x0 : defaults.expr (type.base base.type.nat) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option nat) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun _ : Z => None
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun v0 : nat => Some v0
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option nat)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun _ : Z => None
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun v0 : nat => Some v0
                      end v
                  | _ => None
                  end
                with
                | Some args0 =>
                    UnderLets.Base
                      (fold_right
                         (fun (x1 : defaults.expr (type.base base.type.nat))
                            (xs : defaults.expr
                                    (type.base (base.type.list base.type.nat)))
                          => (x1 :: xs)%expr_pat) []%expr_pat
                         (map (fun v : nat => ##(v)%expr) (seq args args0)))
                | None =>
                    UnderLets.Base (#(ident.List_seq)%expr @ x @ x0)%expr_pat
                end
            | _ => UnderLets.Base (#(ident.List_seq)%expr @ x @ x0)%expr_pat
            end
        | None => UnderLets.Base (#(ident.List_seq)%expr @ x @ x0)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.List_seq)%expr @ x @ x0)%expr_pat
    end
| @ident.List_firstn A =>
    fun (x : defaults.expr (type.base base.type.nat))
      (x0 : defaults.expr (type.base (base.type.list A))) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option nat) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun _ : Z => None
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun v0 : nat => Some v0
              end v
          | _ => None
          end
        with
        | Some args =>
            reflect_list_cps x0
              (fun xs : option (list (defaults.expr (type.base A))) =>
               match xs with
               | Some xs0 =>
                   base.try_make_transport_cps
                     (fun A0 : base.type =>
                      defaults.expr (type.base (base.type.list A0))) A A
                     (UnderLets.UnderLets base.type ident var
                        (defaults.expr (type.base (base.type.list A))))
                     (fun
                        a : option
                              (defaults.expr (type.base (base.type.list A)) ->
                               defaults.expr (type.base (base.type.list A)))
                      =>
                      match a with
                      | Some x' =>
                          UnderLets.Base (x' (reify_list (firstn args xs0)))
                      | None =>
                          UnderLets.Base
                            (#(ident.List_firstn)%expr @ x @ x0)%expr_pat
                      end)
               | None =>
                   UnderLets.Base
                     (#(ident.List_firstn)%expr @ x @ x0)%expr_pat
               end)
        | None =>
            UnderLets.Base (#(ident.List_firstn)%expr @ x @ x0)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.List_firstn)%expr @ x @ x0)%expr_pat
    end
| @ident.List_skipn A =>
    fun (x : defaults.expr (type.base base.type.nat))
      (x0 : defaults.expr (type.base (base.type.list A))) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option nat) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun _ : Z => None
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun v0 : nat => Some v0
              end v
          | _ => None
          end
        with
        | Some args =>
            reflect_list_cps x0
              (fun xs : option (list (defaults.expr (type.base A))) =>
               match xs with
               | Some xs0 =>
                   base.try_make_transport_cps
                     (fun A0 : base.type =>
                      defaults.expr (type.base (base.type.list A0))) A A
                     (UnderLets.UnderLets base.type ident var
                        (defaults.expr (type.base (base.type.list A))))
                     (fun
                        a : option
                              (defaults.expr (type.base (base.type.list A)) ->
                               defaults.expr (type.base (base.type.list A)))
                      =>
                      match a with
                      | Some x' =>
                          UnderLets.Base (x' (reify_list (skipn args xs0)))
                      | None =>
                          UnderLets.Base
                            (#(ident.List_skipn)%expr @ x @ x0)%expr_pat
                      end)
               | None =>
                   UnderLets.Base
                     (#(ident.List_skipn)%expr @ x @ x0)%expr_pat
               end)
        | None => UnderLets.Base (#(ident.List_skipn)%expr @ x @ x0)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.List_skipn)%expr @ x @ x0)%expr_pat
    end
| @ident.List_repeat A =>
    fun (x : defaults.expr (type.base A))
      (x0 : defaults.expr (type.base base.type.nat)) =>
    match x0 with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option nat) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun _ : Z => None
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun v0 : nat => Some v0
              end v
          | _ => None
          end
        with
        | Some args =>
            base.try_make_transport_cps
              (fun A0 : base.type =>
               defaults.expr (type.base (base.type.list A0))) A A
              (UnderLets.UnderLets base.type ident var
                 (defaults.expr (type.base (base.type.list A))))
              (fun
                 a : option
                       (defaults.expr (type.base (base.type.list A)) ->
                        defaults.expr (type.base (base.type.list A))) =>
               match a with
               | Some x' => UnderLets.Base (x' (reify_list (repeat x args)))
               | None =>
                   UnderLets.Base
                     (#(ident.List_repeat)%expr @ x @ x0)%expr_pat
               end)
        | None =>
            UnderLets.Base (#(ident.List_repeat)%expr @ x @ x0)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.List_repeat)%expr @ x @ x0)%expr_pat
    end
| @ident.List_combine A B =>
    fun (x : defaults.expr (type.base (base.type.list A)))
      (x0 : defaults.expr (type.base (base.type.list B))) =>
    reflect_list_cps x
      (fun xs : option (list (defaults.expr (type.base A))) =>
       match xs with
       | Some xs0 =>
           reflect_list_cps x0
             (fun ys : option (list (defaults.expr (type.base B))) =>
              match ys with
              | Some ys0 =>
                  (trA <-- base.try_make_transport_cps
                             (fun A0 : base.type =>
                              defaults.expr
                                (type.base (base.type.list (A0 * B)))) A A;
                   trB <-- base.try_make_transport_cps
                             (fun B0 : base.type =>
                              defaults.expr
                                (type.base (base.type.list (A * B0)))) B B;
                   return Some
                            (fun
                               v : defaults.expr
                                     (type.base (base.type.list (A * B))) =>
                             trB (trA v)))%cps
                    (UnderLets.UnderLets base.type ident var
                       (defaults.expr (type.base (base.type.list (A * B)))))
                    (fun
                       a : option
                             (defaults.expr
                                (type.base (base.type.list (A * B))) ->
                              defaults.expr
                                (type.base (base.type.list (A * B)))) =>
                     match a with
                     | Some x' =>
                         UnderLets.Base
                           (x'
                              (reify_list
                                 (map (fun '(x1, y) => (x1, y)%expr_pat)
                                    (combine xs0 ys0))))
                     | None =>
                         UnderLets.Base
                           (#(ident.List_combine)%expr @ x @ x0)%expr_pat
                     end)
              | None =>
                  UnderLets.Base
                    (#(ident.List_combine)%expr @ x @ x0)%expr_pat
              end)
       | None =>
           UnderLets.Base (#(ident.List_combine)%expr @ x @ x0)%expr_pat
       end)
| @ident.List_map A B =>
    fun
      (x : defaults.expr (type.base A) ->
           UnderLets.UnderLets base.type ident var
             (defaults.expr (type.base B)))
      (x0 : defaults.expr (type.base (base.type.list A))) =>
    Compile.castbe x0
      (UnderLets.UnderLets base.type ident var
         (defaults.expr (type.base (base.type.list B))))
      (fun e : option (defaults.expr (type.base (base.type.list A))) =>
       match e with
       | Some e0 =>
           reflect_list_cps e0
             (fun ls : option (list (defaults.expr (type.base A))) =>
              match ls with
              | Some ls0 =>
                  (fv <-- (e1 <-- list_rect
                                    (fun
                                       _ : list (defaults.expr (type.base A))
                                     =>
                                     UnderLets.UnderLets base.type ident var
                                       (defaults.expr
                                          (type.base (base.type.list B))))
                                    (UnderLets.Base []%expr_pat)
                                    (fun (x1 : defaults.expr (type.base A))
                                       (_ : list
                                              (defaults.expr (type.base A)))
                                       (rec : UnderLets.UnderLets base.type
                                                ident var
                                                (defaults.expr
                                                   (type.base
                                                      (base.type.list B))))
                                     =>
                                     rec' <-- rec;
                                     fx <-- x x1;
                                     UnderLets.Base (fx :: rec')%expr_pat)
                                    ls0;
                           UnderLets.Base
                             {|
                             anyexpr_ty := base.type.list B;
                             unwrap := e1 |});
                   base.try_make_transport_cps
                     (fun t : base.type => defaults.expr (type.base t))
                     (let (anyexpr_ty, _) := fv in anyexpr_ty)
                     (base.type.list B)
                     (UnderLets.UnderLets base.type ident var
                        (defaults.expr (type.base (base.type.list B))))
                     (fun
                        a : option
                              (defaults.expr
                                 (type.base
                                    (let (anyexpr_ty, _) := fv in anyexpr_ty)) ->
                               defaults.expr (type.base (base.type.list B)))
                      =>
                      match a with
                      | Some x' =>
                          UnderLets.Base
                            (x'
                               (let
                                  (anyexpr_ty, unwrap) as a0
                                   return
                                     (defaults.expr
                                        (type.base
                                           (let (anyexpr_ty, _) := a0 in
                                            anyexpr_ty))) := fv in
                                unwrap))
                      | None =>
                          UnderLets.Base
                            (#(ident.List_map)%expr @
                             (λ x1 : var (type.base A),
                              UnderLets.to_expr (x ($x1)))%expr @ x0)%expr_pat
                      end))%under_lets
              | None =>
                  UnderLets.Base
                    (#(ident.List_map)%expr @
                     (λ x1 : var (type.base A),
                      UnderLets.to_expr (x ($x1)))%expr @ x0)%expr_pat
              end)
       | None =>
           UnderLets.Base
             (#(ident.List_map)%expr @
              (λ x1 : var (type.base A),
               UnderLets.to_expr (x ($x1)))%expr @ x0)%expr_pat
       end)
| @ident.List_app A =>
    fun x x0 : defaults.expr (type.base (base.type.list A)) =>
    Compile.castbe x
      (UnderLets.UnderLets base.type ident var
         (defaults.expr (type.base (base.type.list A))))
      (fun e : option (defaults.expr (type.base (base.type.list A))) =>
       match e with
       | Some e0 =>
           reflect_list_cps e0
             (fun ls : option (list (defaults.expr (type.base A))) =>
              match ls with
              | Some ls0 =>
                  (fv <-- (e1 <-- list_rect
                                    (fun
                                       _ : list (defaults.expr (type.base A))
                                     =>
                                     UnderLets.UnderLets base.type ident var
                                       (defaults.expr
                                          (type.base (base.type.list A))))
                                    (UnderLets.Base x0)
                                    (fun (x1 : defaults.expr (type.base A))
                                       (_ : list
                                              (defaults.expr (type.base A)))
                                       (rec : UnderLets.UnderLets base.type
                                                ident var
                                                (defaults.expr
                                                   (type.base
                                                      (base.type.list A))))
                                     =>
                                     rec' <-- rec;
                                     UnderLets.Base (x1 :: rec')%expr_pat)
                                    ls0;
                           UnderLets.Base
                             {|
                             anyexpr_ty := base.type.list A;
                             unwrap := e1 |});
                   base.try_make_transport_cps
                     (fun t : base.type => defaults.expr (type.base t))
                     (let (anyexpr_ty, _) := fv in anyexpr_ty)
                     (base.type.list A)
                     (UnderLets.UnderLets base.type ident var
                        (defaults.expr (type.base (base.type.list A))))
                     (fun
                        a : option
                              (defaults.expr
                                 (type.base
                                    (let (anyexpr_ty, _) := fv in anyexpr_ty)) ->
                               defaults.expr (type.base (base.type.list A)))
                      =>
                      match a with
                      | Some x' =>
                          UnderLets.Base
                            (x'
                               (let
                                  (anyexpr_ty, unwrap) as a0
                                   return
                                     (defaults.expr
                                        (type.base
                                           (let (anyexpr_ty, _) := a0 in
                                            anyexpr_ty))) := fv in
                                unwrap))
                      | None => UnderLets.Base (x ++ x0)%expr
                      end))%under_lets
              | None => UnderLets.Base (x ++ x0)%expr
              end)
       | None => UnderLets.Base (x ++ x0)%expr
       end)
| @ident.List_rev A =>
    fun x : defaults.expr (type.base (base.type.list A)) =>
    reflect_list_cps x
      (fun xs : option (list (defaults.expr (type.base A))) =>
       match xs with
       | Some xs0 =>
           base.try_make_transport_cps
             (fun A0 : base.type =>
              defaults.expr (type.base (base.type.list A0))) A A
             (UnderLets.UnderLets base.type ident var
                (defaults.expr (type.base (base.type.list A))))
             (fun
                a : option
                      (defaults.expr (type.base (base.type.list A)) ->
                       defaults.expr (type.base (base.type.list A))) =>
              match a with
              | Some x' => UnderLets.Base (x' (reify_list (rev xs0)))
              | None => UnderLets.Base (#(ident.List_rev)%expr @ x)%expr_pat
              end)
       | None => UnderLets.Base (#(ident.List_rev)%expr @ x)%expr_pat
       end)
| @ident.List_flat_map A B =>
    fun
      (x : defaults.expr (type.base A) ->
           UnderLets.UnderLets base.type ident var
             (defaults.expr (type.base (base.type.list B))))
      (x0 : defaults.expr (type.base (base.type.list A))) =>
    Compile.castbe x0
      (UnderLets.UnderLets base.type ident var
         (defaults.expr (type.base (base.type.list B))))
      (fun e : option (defaults.expr (type.base (base.type.list A))) =>
       match e with
       | Some e0 =>
           reflect_list_cps e0
             (fun ls : option (list (defaults.expr (type.base A))) =>
              match ls with
              | Some ls0 =>
                  (fv <-- (e1 <-- list_rect
                                    (fun
                                       _ : list (defaults.expr (type.base A))
                                     =>
                                     UnderLets.UnderLets base.type ident var
                                       (defaults.expr
                                          (type.base (base.type.list B))))
                                    (UnderLets.Base []%expr_pat)
                                    (fun (x1 : defaults.expr (type.base A))
                                       (_ : list
                                              (defaults.expr (type.base A)))
                                       (rec : UnderLets.UnderLets base.type
                                                ident var
                                                (defaults.expr
                                                   (type.base
                                                      (base.type.list B))))
                                     =>
                                     rec' <-- rec;
                                     fx <-- x x1;
                                     UnderLets.Base ($fx ++ rec')%expr) ls0;
                           UnderLets.Base
                             {|
                             anyexpr_ty := base.type.list B;
                             unwrap := e1 |});
                   fv0 <-- do_again (let (anyexpr_ty, _) := fv in anyexpr_ty)
                             (let
                                (anyexpr_ty, unwrap) as a
                                 return
                                   (defaults.expr
                                      (type.base
                                         (let (anyexpr_ty, _) := a in
                                          anyexpr_ty))) := fv in
                              unwrap);
                   base.try_make_transport_cps
                     (fun t : base.type => defaults.expr (type.base t))
                     (let (anyexpr_ty, _) := fv in anyexpr_ty)
                     (base.type.list B)
                     (UnderLets.UnderLets base.type ident var
                        (defaults.expr (type.base (base.type.list B))))
                     (fun
                        a : option
                              (defaults.expr
                                 (type.base
                                    (let (anyexpr_ty, _) := fv in anyexpr_ty)) ->
                               defaults.expr (type.base (base.type.list B)))
                      =>
                      match a with
                      | Some x' => UnderLets.Base (x' fv0)
                      | None =>
                          UnderLets.Base
                            (#(ident.List_flat_map)%expr @
                             (λ x1 : var (type.base A),
                              UnderLets.to_expr (x ($x1)))%expr @ x0)%expr_pat
                      end))%under_lets
              | None =>
                  UnderLets.Base
                    (#(ident.List_flat_map)%expr @
                     (λ x1 : var (type.base A),
                      UnderLets.to_expr (x ($x1)))%expr @ x0)%expr_pat
              end)
       | None =>
           UnderLets.Base
             (#(ident.List_flat_map)%expr @
              (λ x1 : var (type.base A),
               UnderLets.to_expr (x ($x1)))%expr @ x0)%expr_pat
       end)
| @ident.List_partition A =>
    fun
      (x : defaults.expr (type.base A) ->
           UnderLets.UnderLets base.type ident var
             (defaults.expr (type.base base.type.bool)))
      (x0 : defaults.expr (type.base (base.type.list A))) =>
    Compile.castbe x0
      (UnderLets.UnderLets base.type ident var
         (defaults.expr
            (type.base (base.type.list A * base.type.list A)%etype)))
      (fun e : option (defaults.expr (type.base (base.type.list A))) =>
       match e with
       | Some e0 =>
           reflect_list_cps e0
             (fun ls : option (list (defaults.expr (type.base A))) =>
              match ls with
              | Some ls0 =>
                  (fv <-- (e1 <-- list_rect
                                    (fun
                                       _ : list (defaults.expr (type.base A))
                                     =>
                                     UnderLets.UnderLets base.type ident var
                                       (defaults.expr
                                          (type.base
                                             (base.type.list A *
                                              base.type.list A)%etype)))
                                    (UnderLets.Base ([], [])%expr_pat)
                                    (fun (x1 : defaults.expr (type.base A))
                                       (_ : list
                                              (defaults.expr (type.base A)))
                                       (rec : UnderLets.UnderLets base.type
                                                ident var
                                                (defaults.expr
                                                   (type.base
                                                      (base.type.list A *
                                                       base.type.list A)%etype)))
                                     =>
                                     rec' <-- rec;
                                     fx <-- id x x1;
                                     UnderLets.Base
                                       (#(ident.prod_rect)%expr @
                                        (λ g
                                            d : defaults.expr
                                                  (type.base
                                                     (base.type.list A)),
                                         (#(ident.bool_rect)%expr @
                                          (λ _ : defaults.expr
                                                   (type.base base.type.unit),
                                           ($x1 :: $g, $d)%expr_pat) @
                                          (λ _ : defaults.expr
                                                   (type.base base.type.unit),
                                           ($g, $x1 :: $d)%expr_pat) @ $fx)%expr_pat)%expr @
                                        rec')%expr_pat) ls0;
                           UnderLets.Base
                             {|
                             anyexpr_ty := (base.type.list A *
                                            base.type.list A)%etype;
                             unwrap := e1 |});
                   fv0 <-- do_again (let (anyexpr_ty, _) := fv in anyexpr_ty)
                             (let
                                (anyexpr_ty, unwrap) as a
                                 return
                                   (defaults.expr
                                      (type.base
                                         (let (anyexpr_ty, _) := a in
                                          anyexpr_ty))) := fv in
                              unwrap);
                   base.try_make_transport_cps
                     (fun t : base.type => defaults.expr (type.base t))
                     (let (anyexpr_ty, _) := fv in anyexpr_ty)
                     (base.type.list A * base.type.list A)
                     (UnderLets.UnderLets base.type ident var
                        (defaults.expr
                           (type.base
                              (base.type.list A * base.type.list A)%etype)))
                     (fun
                        a : option
                              (defaults.expr
                                 (type.base
                                    (let (anyexpr_ty, _) := fv in anyexpr_ty)) ->
                               defaults.expr
                                 (type.base
                                    (base.type.list A * base.type.list A)%etype))
                      =>
                      match a with
                      | Some x' => UnderLets.Base (x' fv0)
                      | None =>
                          UnderLets.Base
                            (#(ident.List_partition)%expr @
                             (λ x1 : var (type.base A),
                              UnderLets.to_expr (x ($x1)))%expr @ x0)%expr_pat
                      end))%under_lets
              | None =>
                  UnderLets.Base
                    (#(ident.List_partition)%expr @
                     (λ x1 : var (type.base A),
                      UnderLets.to_expr (x ($x1)))%expr @ x0)%expr_pat
              end)
       | None =>
           UnderLets.Base
             (#(ident.List_partition)%expr @
              (λ x1 : var (type.base A),
               UnderLets.to_expr (x ($x1)))%expr @ x0)%expr_pat
       end)
| @ident.List_fold_right A B =>
    fun
      (x : defaults.expr (type.base B) ->
           defaults.expr (type.base A) ->
           UnderLets.UnderLets base.type ident var
             (defaults.expr (type.base A)))
      (x0 : defaults.expr (type.base A))
      (x1 : defaults.expr (type.base (base.type.list B))) =>
    Compile.castv x
      (UnderLets.UnderLets base.type ident var (defaults.expr (type.base A)))
      (fun
         f : option
               (defaults.expr (type.base B) ->
                defaults.expr (type.base A) ->
                UnderLets.UnderLets base.type ident var
                  (defaults.expr (type.base A))) =>
       match f with
       | Some f0 =>
           reflect_list_cps x1
             (fun ls : option (list (defaults.expr (type.base B))) =>
              match ls with
              | Some ls0 =>
                  (fv <-- (e <-- list_rect
                                   (fun
                                      _ : list (defaults.expr (type.base B))
                                    =>
                                    UnderLets.UnderLets base.type ident var
                                      (defaults.expr (type.base A)))
                                   (UnderLets.Base x0)
                                   (fun (x2 : defaults.expr (type.base B))
                                      (_ : list (defaults.expr (type.base B)))
                                      (rec : UnderLets.UnderLets base.type
                                               ident var
                                               (defaults.expr (type.base A)))
                                    => rec' <-- rec;
                                       f0 x2 rec') ls0;
                           UnderLets.Base {| anyexpr_ty := A; unwrap := e |});
                   base.try_make_transport_cps
                     (fun t : base.type => defaults.expr (type.base t))
                     (let (anyexpr_ty, _) := fv in anyexpr_ty) A
                     (UnderLets.UnderLets base.type ident var
                        (defaults.expr (type.base A)))
                     (fun
                        a : option
                              (defaults.expr
                                 (type.base
                                    (let (anyexpr_ty, _) := fv in anyexpr_ty)) ->
                               defaults.expr (type.base A)) =>
                      match a with
                      | Some x' =>
                          UnderLets.Base
                            (x'
                               (let
                                  (anyexpr_ty, unwrap) as a0
                                   return
                                     (defaults.expr
                                        (type.base
                                           (let (anyexpr_ty, _) := a0 in
                                            anyexpr_ty))) := fv in
                                unwrap))
                      | None =>
                          UnderLets.Base
                            (#(ident.List_fold_right)%expr @
                             (λ (x2 : var (type.base B))(x3 : var
                                                                (type.base A)),
                              UnderLets.to_expr (x ($x2) ($x3)))%expr @ x0 @
                             x1)%expr_pat
                      end))%under_lets
              | None =>
                  UnderLets.Base
                    (#(ident.List_fold_right)%expr @
                     (λ (x2 : var (type.base B))(x3 : var (type.base A)),
                      UnderLets.to_expr (x ($x2) ($x3)))%expr @ x0 @ x1)%expr_pat
              end)
       | None =>
           UnderLets.Base
             (#(ident.List_fold_right)%expr @
              (λ (x2 : var (type.base B))(x3 : var (type.base A)),
               UnderLets.to_expr (x ($x2) ($x3)))%expr @ x0 @ x1)%expr_pat
       end)
| @ident.List_update_nth T =>
    fun (x : defaults.expr (type.base base.type.nat))
      (x0 : defaults.expr (type.base T) ->
            UnderLets.UnderLets base.type ident var
              (defaults.expr (type.base T)))
      (x1 : defaults.expr (type.base (base.type.list T))) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option nat) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun _ : Z => None
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun v0 : nat => Some v0
              end v
          | _ => None
          end
        with
        | Some args =>
            Compile.castv x0
              (UnderLets.UnderLets base.type ident var
                 (defaults.expr (type.base (base.type.list T))))
              (fun
                 f : option
                       (defaults.expr (type.base T) ->
                        UnderLets.UnderLets base.type ident var
                          (defaults.expr (type.base T))) =>
               match f with
               | Some f0 =>
                   reflect_list_cps x1
                     (fun ls : option (list (defaults.expr (type.base T))) =>
                      match ls with
                      | Some ls0 =>
                          (fv <-- (e <-- (retv <---- update_nth args
                                                       (fun
                                                          x2 : UnderLets.UnderLets
                                                                 base.type
                                                                 ident var
                                                                 (defaults.expr
                                                                    (type.base
                                                                    T)) =>
                                                        x3 <-- x2;
                                                        f0 x3)
                                                       (map UnderLets.Base
                                                          ls0);
                                          UnderLets.Base (reify_list retv));
                                   UnderLets.Base
                                     {|
                                     anyexpr_ty := base.type.list T;
                                     unwrap := e |});
                           base.try_make_transport_cps
                             (fun t0 : base.type =>
                              defaults.expr (type.base t0))
                             (let (anyexpr_ty, _) := fv in anyexpr_ty)
                             (base.type.list T)
                             (UnderLets.UnderLets base.type ident var
                                (defaults.expr (type.base (base.type.list T))))
                             (fun
                                a : option
                                      (defaults.expr
                                         (type.base
                                            (let (anyexpr_ty, _) := fv in
                                             anyexpr_ty)) ->
                                       defaults.expr
                                         (type.base (base.type.list T))) =>
                              match a with
                              | Some x' =>
                                  UnderLets.Base
                                    (x'
                                       (let
                                          (anyexpr_ty, unwrap) as a0
                                           return
                                             (defaults.expr
                                                (type.base
                                                   (let (anyexpr_ty, _) :=
                                                      a0 in
                                                    anyexpr_ty))) := fv in
                                        unwrap))
                              | None =>
                                  UnderLets.Base
                                    (#(ident.List_update_nth)%expr @ x @
                                     (λ x2 : var (type.base T),
                                      UnderLets.to_expr (x0 ($x2)))%expr @ x1)%expr_pat
                              end))%under_lets
                      | None =>
                          UnderLets.Base
                            (#(ident.List_update_nth)%expr @ x @
                             (λ x2 : var (type.base T),
                              UnderLets.to_expr (x0 ($x2)))%expr @ x1)%expr_pat
                      end)
               | None =>
                   UnderLets.Base
                     (#(ident.List_update_nth)%expr @ x @
                      (λ x2 : var (type.base T),
                       UnderLets.to_expr (x0 ($x2)))%expr @ x1)%expr_pat
               end)
        | None =>
            UnderLets.Base
              (#(ident.List_update_nth)%expr @ x @
               (λ x2 : var (type.base T),
                UnderLets.to_expr (x0 ($x2)))%expr @ x1)%expr_pat
        end
    | ($_)%expr | @expr.Abs _ _ _ _ _ _ =>
        UnderLets.Base
          (#(ident.List_update_nth)%expr @ x @
           (λ x2 : var (type.base T),
            UnderLets.to_expr (x0 ($x2)))%expr @ x1)%expr_pat
    | _ =>
        UnderLets.Base
          (#(ident.List_update_nth)%expr @ x @
           (λ x3 : var (type.base T),
            UnderLets.to_expr (x0 ($x3)))%expr @ x1)%expr_pat
    end
| @ident.List_nth_default T =>
    fun (x : defaults.expr (type.base T))
      (x0 : defaults.expr (type.base (base.type.list T)))
      (x1 : defaults.expr (type.base base.type.nat)) =>
    match x1 with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option nat) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun _ : Z => None
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun v0 : nat => Some v0
              end v
          | _ => None
          end
        with
        | Some args =>
            Compile.castbe x
              (UnderLets.UnderLets base.type ident var
                 (defaults.expr (type.base T)))
              (fun default : option (defaults.expr (type.base T)) =>
               match default with
               | Some default0 =>
                   reflect_list_cps x0
                     (fun ls : option (list (defaults.expr (type.base T))) =>
                      match ls with
                      | Some ls0 =>
                          base.try_make_transport_cps
                            (fun t0 : base.type =>
                             defaults.expr (type.base t0)) T T
                            (UnderLets.UnderLets base.type ident var
                               (defaults.expr (type.base T)))
                            (fun
                               a : option
                                     (defaults.expr (type.base T) ->
                                      defaults.expr (type.base T)) =>
                             match a with
                             | Some x' =>
                                 UnderLets.Base
                                   (x' (nth_default default0 ls0 args))
                             | None =>
                                 UnderLets.Base
                                   (#(ident.List_nth_default)%expr @ x @ x0 @
                                    x1)%expr_pat
                             end)
                      | None =>
                          UnderLets.Base
                            (#(ident.List_nth_default)%expr @ x @ x0 @ x1)%expr_pat
                      end)
               | None =>
                   UnderLets.Base
                     (#(ident.List_nth_default)%expr @ x @ x0 @ x1)%expr_pat
               end)
        | None =>
            UnderLets.Base
              (#(ident.List_nth_default)%expr @ x @ x0 @ x1)%expr_pat
        end
    | _ =>
        UnderLets.Base
          (#(ident.List_nth_default)%expr @ x @ x0 @ x1)%expr_pat
    end
| ident.Z_add =>
    fun x x0 : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 => UnderLets.Base ##((args + args0)%Z)%expr
                | None => UnderLets.Base (x + x0)%expr
                end
            | _ => UnderLets.Base (x + x0)%expr
            end
        | None => UnderLets.Base (x + x0)%expr
        end
    | _ => UnderLets.Base (x + x0)%expr
    end
| ident.Z_mul =>
    fun x x0 : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 => UnderLets.Base ##((args * args0)%Z)%expr
                | None => UnderLets.Base (x * x0)%expr
                end
            | _ => UnderLets.Base (x * x0)%expr
            end
        | None => UnderLets.Base (x * x0)%expr
        end
    | _ => UnderLets.Base (x * x0)%expr
    end
| ident.Z_pow =>
    fun x x0 : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 => UnderLets.Base ##(args ^ args0)%expr
                | None =>
                    UnderLets.Base (#(ident.Z_pow)%expr @ x @ x0)%expr_pat
                end
            | _ => UnderLets.Base (#(ident.Z_pow)%expr @ x @ x0)%expr_pat
            end
        | None => UnderLets.Base (#(ident.Z_pow)%expr @ x @ x0)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.Z_pow)%expr @ x @ x0)%expr_pat
    end
| ident.Z_sub =>
    fun x x0 : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 => UnderLets.Base ##((args - args0)%Z)%expr
                | None => UnderLets.Base (x - x0)%expr
                end
            | _ => UnderLets.Base (x - x0)%expr
            end
        | None => UnderLets.Base (x - x0)%expr
        end
    | _ => UnderLets.Base (x - x0)%expr
    end
| ident.Z_opp =>
    fun x : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args => UnderLets.Base ##((- args)%Z)%expr
        | None => UnderLets.Base (- x)%expr
        end
    | _ => UnderLets.Base (- x)%expr
    end
| ident.Z_div =>
    fun x x0 : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 => UnderLets.Base ##((args / args0)%Z)%expr
                | None => UnderLets.Base (x / x0)%expr
                end
            | _ => UnderLets.Base (x / x0)%expr
            end
        | None => UnderLets.Base (x / x0)%expr
        end
    | _ => UnderLets.Base (x / x0)%expr
    end
| ident.Z_modulo =>
    fun x x0 : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 => UnderLets.Base ##((args mod args0)%Z)%expr
                | None => UnderLets.Base (x mod x0)%expr
                end
            | _ => UnderLets.Base (x mod x0)%expr
            end
        | None => UnderLets.Base (x mod x0)%expr
        end
    | _ => UnderLets.Base (x mod x0)%expr
    end
| ident.Z_log2 =>
    fun x : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args => UnderLets.Base ##(Z.log2 args)%expr
        | None => UnderLets.Base (#(ident.Z_log2)%expr @ x)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.Z_log2)%expr @ x)%expr_pat
    end
| ident.Z_log2_up =>
    fun x : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args => UnderLets.Base ##(Z.log2_up args)%expr
        | None => UnderLets.Base (#(ident.Z_log2_up)%expr @ x)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.Z_log2_up)%expr @ x)%expr_pat
    end
| ident.Z_eqb =>
    fun x x0 : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 => UnderLets.Base ##(args =? args0)%expr
                | None =>
                    UnderLets.Base (#(ident.Z_eqb)%expr @ x @ x0)%expr_pat
                end
            | _ => UnderLets.Base (#(ident.Z_eqb)%expr @ x @ x0)%expr_pat
            end
        | None => UnderLets.Base (#(ident.Z_eqb)%expr @ x @ x0)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.Z_eqb)%expr @ x @ x0)%expr_pat
    end
| ident.Z_leb =>
    fun x x0 : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 => UnderLets.Base ##(args <=? args0)%expr
                | None =>
                    UnderLets.Base (#(ident.Z_leb)%expr @ x @ x0)%expr_pat
                end
            | _ => UnderLets.Base (#(ident.Z_leb)%expr @ x @ x0)%expr_pat
            end
        | None => UnderLets.Base (#(ident.Z_leb)%expr @ x @ x0)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.Z_leb)%expr @ x @ x0)%expr_pat
    end
| ident.Z_geb =>
    fun x x0 : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 => UnderLets.Base ##(args >=? args0)%expr
                | None =>
                    UnderLets.Base (#(ident.Z_geb)%expr @ x @ x0)%expr_pat
                end
            | _ => UnderLets.Base (#(ident.Z_geb)%expr @ x @ x0)%expr_pat
            end
        | None => UnderLets.Base (#(ident.Z_geb)%expr @ x @ x0)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.Z_geb)%expr @ x @ x0)%expr_pat
    end
| ident.Z_of_nat =>
    fun x : defaults.expr (type.base base.type.nat) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option nat) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun _ : Z => None
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun v0 : nat => Some v0
              end v
          | _ => None
          end
        with
        | Some args => UnderLets.Base ##(Z.of_nat args)%expr
        | None => UnderLets.Base (#(ident.Z_of_nat)%expr @ x)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.Z_of_nat)%expr @ x)%expr_pat
    end
| ident.Z_to_nat =>
    fun x : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args => UnderLets.Base ##(Z.to_nat args)%expr
        | None => UnderLets.Base (#(ident.Z_to_nat)%expr @ x)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.Z_to_nat)%expr @ x)%expr_pat
    end
| ident.Z_shiftr =>
    fun x x0 : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 => UnderLets.Base ##(Z.shiftr args args0)%expr
                | None => UnderLets.Base (x >> x0)%expr
                end
            | _ => UnderLets.Base (x >> x0)%expr
            end
        | None => UnderLets.Base (x >> x0)%expr
        end
    | _ => UnderLets.Base (x >> x0)%expr
    end
| ident.Z_shiftl =>
    fun x x0 : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 => UnderLets.Base ##(Z.shiftl args args0)%expr
                | None => UnderLets.Base (x << x0)%expr
                end
            | _ => UnderLets.Base (x << x0)%expr
            end
        | None => UnderLets.Base (x << x0)%expr
        end
    | _ => UnderLets.Base (x << x0)%expr
    end
| ident.Z_land =>
    fun x x0 : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 => UnderLets.Base ##(Z.land args args0)%expr
                | None => UnderLets.Base (x &' x0)%expr
                end
            | _ => UnderLets.Base (x &' x0)%expr
            end
        | None => UnderLets.Base (x &' x0)%expr
        end
    | _ => UnderLets.Base (x &' x0)%expr
    end
| ident.Z_lor =>
    fun x x0 : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 => UnderLets.Base ##(Z.lor args args0)%expr
                | None => UnderLets.Base (x || x0)%expr
                end
            | _ => UnderLets.Base (x || x0)%expr
            end
        | None => UnderLets.Base (x || x0)%expr
        end
    | _ => UnderLets.Base (x || x0)%expr
    end
| ident.Z_bneg =>
    fun x : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args => UnderLets.Base ##(Definitions.Z.bneg args)%expr
        | None => UnderLets.Base (#(ident.Z_bneg)%expr @ x)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.Z_bneg)%expr @ x)%expr_pat
    end
| ident.Z_lnot_modulo =>
    fun x x0 : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 =>
                    UnderLets.Base
                      ##(Definitions.Z.lnot_modulo args args0)%expr
                | None =>
                    UnderLets.Base
                      (#(ident.Z_lnot_modulo)%expr @ x @ x0)%expr_pat
                end
            | _ =>
                UnderLets.Base
                  (#(ident.Z_lnot_modulo)%expr @ x @ x0)%expr_pat
            end
        | None =>
            UnderLets.Base (#(ident.Z_lnot_modulo)%expr @ x @ x0)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.Z_lnot_modulo)%expr @ x @ x0)%expr_pat
    end
| ident.Z_mul_split =>
    fun x x0 x1 : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 =>
                    match x1 with
                    | #(idc1)%expr_pat =>
                        match
                          match idc1 with
                          | @ident.Literal t2 v =>
                              match
                                t2 as t3
                                return (base.base_interp t3 -> option Z)
                              with
                              | base.type.unit => fun _ : unit => None
                              | base.type.Z => fun v0 : Z => Some v0
                              | base.type.bool => fun _ : bool => None
                              | base.type.nat => fun _ : nat => None
                              end v
                          | _ => None
                          end
                        with
                        | Some args1 =>
                            UnderLets.Base
                              (let
                               '(a, b) :=
                                Definitions.Z.mul_split args args0 args1 in
                                (##(a)%expr, ##(b)%expr)%expr_pat)
                        | None =>
                            UnderLets.Base
                              (#(ident.Z_mul_split)%expr @ x @ x0 @ x1)%expr_pat
                        end
                    | _ =>
                        UnderLets.Base
                          (#(ident.Z_mul_split)%expr @ x @ x0 @ x1)%expr_pat
                    end
                | None =>
                    UnderLets.Base
                      (#(ident.Z_mul_split)%expr @ x @ x0 @ x1)%expr_pat
                end
            | _ =>
                UnderLets.Base
                  (#(ident.Z_mul_split)%expr @ x @ x0 @ x1)%expr_pat
            end
        | None =>
            UnderLets.Base (#(ident.Z_mul_split)%expr @ x @ x0 @ x1)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.Z_mul_split)%expr @ x @ x0 @ x1)%expr_pat
    end
| ident.Z_add_get_carry =>
    fun x x0 x1 : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 =>
                    match x1 with
                    | #(idc1)%expr_pat =>
                        match
                          match idc1 with
                          | @ident.Literal t2 v =>
                              match
                                t2 as t3
                                return (base.base_interp t3 -> option Z)
                              with
                              | base.type.unit => fun _ : unit => None
                              | base.type.Z => fun v0 : Z => Some v0
                              | base.type.bool => fun _ : bool => None
                              | base.type.nat => fun _ : nat => None
                              end v
                          | _ => None
                          end
                        with
                        | Some args1 =>
                            UnderLets.Base
                              (let
                               '(a, b) :=
                                Definitions.Z.add_get_carry_full args args0
                                  args1 in (##(a)%expr, ##(b)%expr)%expr_pat)
                        | None =>
                            UnderLets.Base
                              (#(ident.Z_add_get_carry)%expr @ x @ x0 @ x1)%expr_pat
                        end
                    | _ =>
                        UnderLets.Base
                          (#(ident.Z_add_get_carry)%expr @ x @ x0 @ x1)%expr_pat
                    end
                | None =>
                    UnderLets.Base
                      (#(ident.Z_add_get_carry)%expr @ x @ x0 @ x1)%expr_pat
                end
            | _ =>
                UnderLets.Base
                  (#(ident.Z_add_get_carry)%expr @ x @ x0 @ x1)%expr_pat
            end
        | None =>
            UnderLets.Base
              (#(ident.Z_add_get_carry)%expr @ x @ x0 @ x1)%expr_pat
        end
    | _ =>
        UnderLets.Base (#(ident.Z_add_get_carry)%expr @ x @ x0 @ x1)%expr_pat
    end
| ident.Z_add_with_carry =>
    fun x x0 x1 : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 =>
                    match x1 with
                    | #(idc1)%expr_pat =>
                        match
                          match idc1 with
                          | @ident.Literal t2 v =>
                              match
                                t2 as t3
                                return (base.base_interp t3 -> option Z)
                              with
                              | base.type.unit => fun _ : unit => None
                              | base.type.Z => fun v0 : Z => Some v0
                              | base.type.bool => fun _ : bool => None
                              | base.type.nat => fun _ : nat => None
                              end v
                          | _ => None
                          end
                        with
                        | Some args1 =>
                            UnderLets.Base
                              ##(Definitions.Z.add_with_carry args args0
                                   args1)%expr
                        | None =>
                            UnderLets.Base
                              (#(ident.Z_add_with_carry)%expr @ x @ x0 @ x1)%expr_pat
                        end
                    | _ =>
                        UnderLets.Base
                          (#(ident.Z_add_with_carry)%expr @ x @ x0 @ x1)%expr_pat
                    end
                | None =>
                    UnderLets.Base
                      (#(ident.Z_add_with_carry)%expr @ x @ x0 @ x1)%expr_pat
                end
            | _ =>
                UnderLets.Base
                  (#(ident.Z_add_with_carry)%expr @ x @ x0 @ x1)%expr_pat
            end
        | None =>
            UnderLets.Base
              (#(ident.Z_add_with_carry)%expr @ x @ x0 @ x1)%expr_pat
        end
    | _ =>
        UnderLets.Base
          (#(ident.Z_add_with_carry)%expr @ x @ x0 @ x1)%expr_pat
    end
| ident.Z_add_with_get_carry =>
    fun x x0 x1 x2 : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 =>
                    match x1 with
                    | #(idc1)%expr_pat =>
                        match
                          match idc1 with
                          | @ident.Literal t2 v =>
                              match
                                t2 as t3
                                return (base.base_interp t3 -> option Z)
                              with
                              | base.type.unit => fun _ : unit => None
                              | base.type.Z => fun v0 : Z => Some v0
                              | base.type.bool => fun _ : bool => None
                              | base.type.nat => fun _ : nat => None
                              end v
                          | _ => None
                          end
                        with
                        | Some args1 =>
                            match x2 with
                            | #(idc2)%expr_pat =>
                                match
                                  match idc2 with
                                  | @ident.Literal t3 v =>
                                      match
                                        t3 as t4
                                        return
                                          (base.base_interp t4 -> option Z)
                                      with
                                      | base.type.unit =>
                                          fun _ : unit => None
                                      | base.type.Z => fun v0 : Z => Some v0
                                      | base.type.bool =>
                                          fun _ : bool => None
                                      | base.type.nat => fun _ : nat => None
                                      end v
                                  | _ => None
                                  end
                                with
                                | Some args2 =>
                                    UnderLets.Base
                                      (let
                                       '(a, b) :=
                                        Definitions.Z.add_with_get_carry_full
                                          args args0 args1 args2 in
                                        (##(a)%expr, ##(b)%expr)%expr_pat)
                                | None =>
                                    UnderLets.Base
                                      (#(ident.Z_add_with_get_carry)%expr @ x @
                                       x0 @ x1 @ x2)%expr_pat
                                end
                            | _ =>
                                UnderLets.Base
                                  (#(ident.Z_add_with_get_carry)%expr @ x @
                                   x0 @ x1 @ x2)%expr_pat
                            end
                        | None =>
                            UnderLets.Base
                              (#(ident.Z_add_with_get_carry)%expr @ x @ x0 @
                               x1 @ x2)%expr_pat
                        end
                    | _ =>
                        UnderLets.Base
                          (#(ident.Z_add_with_get_carry)%expr @ x @ x0 @ x1 @
                           x2)%expr_pat
                    end
                | None =>
                    UnderLets.Base
                      (#(ident.Z_add_with_get_carry)%expr @ x @ x0 @ x1 @ x2)%expr_pat
                end
            | _ =>
                UnderLets.Base
                  (#(ident.Z_add_with_get_carry)%expr @ x @ x0 @ x1 @ x2)%expr_pat
            end
        | None =>
            UnderLets.Base
              (#(ident.Z_add_with_get_carry)%expr @ x @ x0 @ x1 @ x2)%expr_pat
        end
    | _ =>
        UnderLets.Base
          (#(ident.Z_add_with_get_carry)%expr @ x @ x0 @ x1 @ x2)%expr_pat
    end
| ident.Z_sub_get_borrow =>
    fun x x0 x1 : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 =>
                    match x1 with
                    | #(idc1)%expr_pat =>
                        match
                          match idc1 with
                          | @ident.Literal t2 v =>
                              match
                                t2 as t3
                                return (base.base_interp t3 -> option Z)
                              with
                              | base.type.unit => fun _ : unit => None
                              | base.type.Z => fun v0 : Z => Some v0
                              | base.type.bool => fun _ : bool => None
                              | base.type.nat => fun _ : nat => None
                              end v
                          | _ => None
                          end
                        with
                        | Some args1 =>
                            UnderLets.Base
                              (let
                               '(a, b) :=
                                Definitions.Z.sub_get_borrow_full args args0
                                  args1 in (##(a)%expr, ##(b)%expr)%expr_pat)
                        | None =>
                            UnderLets.Base
                              (#(ident.Z_sub_get_borrow)%expr @ x @ x0 @ x1)%expr_pat
                        end
                    | _ =>
                        UnderLets.Base
                          (#(ident.Z_sub_get_borrow)%expr @ x @ x0 @ x1)%expr_pat
                    end
                | None =>
                    UnderLets.Base
                      (#(ident.Z_sub_get_borrow)%expr @ x @ x0 @ x1)%expr_pat
                end
            | _ =>
                UnderLets.Base
                  (#(ident.Z_sub_get_borrow)%expr @ x @ x0 @ x1)%expr_pat
            end
        | None =>
            UnderLets.Base
              (#(ident.Z_sub_get_borrow)%expr @ x @ x0 @ x1)%expr_pat
        end
    | _ =>
        UnderLets.Base
          (#(ident.Z_sub_get_borrow)%expr @ x @ x0 @ x1)%expr_pat
    end
| ident.Z_sub_with_get_borrow =>
    fun x x0 x1 x2 : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 =>
                    match x1 with
                    | #(idc1)%expr_pat =>
                        match
                          match idc1 with
                          | @ident.Literal t2 v =>
                              match
                                t2 as t3
                                return (base.base_interp t3 -> option Z)
                              with
                              | base.type.unit => fun _ : unit => None
                              | base.type.Z => fun v0 : Z => Some v0
                              | base.type.bool => fun _ : bool => None
                              | base.type.nat => fun _ : nat => None
                              end v
                          | _ => None
                          end
                        with
                        | Some args1 =>
                            match x2 with
                            | #(idc2)%expr_pat =>
                                match
                                  match idc2 with
                                  | @ident.Literal t3 v =>
                                      match
                                        t3 as t4
                                        return
                                          (base.base_interp t4 -> option Z)
                                      with
                                      | base.type.unit =>
                                          fun _ : unit => None
                                      | base.type.Z => fun v0 : Z => Some v0
                                      | base.type.bool =>
                                          fun _ : bool => None
                                      | base.type.nat => fun _ : nat => None
                                      end v
                                  | _ => None
                                  end
                                with
                                | Some args2 =>
                                    UnderLets.Base
                                      (let
                                       '(a, b) :=
                                        Definitions.Z.sub_with_get_borrow_full
                                          args args0 args1 args2 in
                                        (##(a)%expr, ##(b)%expr)%expr_pat)
                                | None =>
                                    UnderLets.Base
                                      (#(ident.Z_sub_with_get_borrow)%expr @
                                       x @ x0 @ x1 @ x2)%expr_pat
                                end
                            | _ =>
                                UnderLets.Base
                                  (#(ident.Z_sub_with_get_borrow)%expr @ x @
                                   x0 @ x1 @ x2)%expr_pat
                            end
                        | None =>
                            UnderLets.Base
                              (#(ident.Z_sub_with_get_borrow)%expr @ x @ x0 @
                               x1 @ x2)%expr_pat
                        end
                    | _ =>
                        UnderLets.Base
                          (#(ident.Z_sub_with_get_borrow)%expr @ x @ x0 @ x1 @
                           x2)%expr_pat
                    end
                | None =>
                    UnderLets.Base
                      (#(ident.Z_sub_with_get_borrow)%expr @ x @ x0 @ x1 @ x2)%expr_pat
                end
            | _ =>
                UnderLets.Base
                  (#(ident.Z_sub_with_get_borrow)%expr @ x @ x0 @ x1 @ x2)%expr_pat
            end
        | None =>
            UnderLets.Base
              (#(ident.Z_sub_with_get_borrow)%expr @ x @ x0 @ x1 @ x2)%expr_pat
        end
    | _ =>
        UnderLets.Base
          (#(ident.Z_sub_with_get_borrow)%expr @ x @ x0 @ x1 @ x2)%expr_pat
    end
| ident.Z_zselect =>
    fun x x0 x1 : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 =>
                    match x1 with
                    | #(idc1)%expr_pat =>
                        match
                          match idc1 with
                          | @ident.Literal t2 v =>
                              match
                                t2 as t3
                                return (base.base_interp t3 -> option Z)
                              with
                              | base.type.unit => fun _ : unit => None
                              | base.type.Z => fun v0 : Z => Some v0
                              | base.type.bool => fun _ : bool => None
                              | base.type.nat => fun _ : nat => None
                              end v
                          | _ => None
                          end
                        with
                        | Some args1 =>
                            UnderLets.Base
                              ##(Definitions.Z.zselect args args0 args1)%expr
                        | None =>
                            UnderLets.Base
                              (#(ident.Z_zselect)%expr @ x @ x0 @ x1)%expr_pat
                        end
                    | _ =>
                        UnderLets.Base
                          (#(ident.Z_zselect)%expr @ x @ x0 @ x1)%expr_pat
                    end
                | None =>
                    UnderLets.Base
                      (#(ident.Z_zselect)%expr @ x @ x0 @ x1)%expr_pat
                end
            | _ =>
                UnderLets.Base
                  (#(ident.Z_zselect)%expr @ x @ x0 @ x1)%expr_pat
            end
        | None =>
            UnderLets.Base (#(ident.Z_zselect)%expr @ x @ x0 @ x1)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.Z_zselect)%expr @ x @ x0 @ x1)%expr_pat
    end
| ident.Z_add_modulo =>
    fun x x0 x1 : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 =>
                    match x1 with
                    | #(idc1)%expr_pat =>
                        match
                          match idc1 with
                          | @ident.Literal t2 v =>
                              match
                                t2 as t3
                                return (base.base_interp t3 -> option Z)
                              with
                              | base.type.unit => fun _ : unit => None
                              | base.type.Z => fun v0 : Z => Some v0
                              | base.type.bool => fun _ : bool => None
                              | base.type.nat => fun _ : nat => None
                              end v
                          | _ => None
                          end
                        with
                        | Some args1 =>
                            UnderLets.Base
                              ##(Definitions.Z.add_modulo args args0 args1)%expr
                        | None =>
                            UnderLets.Base
                              (#(ident.Z_add_modulo)%expr @ x @ x0 @ x1)%expr_pat
                        end
                    | _ =>
                        UnderLets.Base
                          (#(ident.Z_add_modulo)%expr @ x @ x0 @ x1)%expr_pat
                    end
                | None =>
                    UnderLets.Base
                      (#(ident.Z_add_modulo)%expr @ x @ x0 @ x1)%expr_pat
                end
            | _ =>
                UnderLets.Base
                  (#(ident.Z_add_modulo)%expr @ x @ x0 @ x1)%expr_pat
            end
        | None =>
            UnderLets.Base
              (#(ident.Z_add_modulo)%expr @ x @ x0 @ x1)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.Z_add_modulo)%expr @ x @ x0 @ x1)%expr_pat
    end
| ident.Z_rshi =>
    fun x x0 x1 x2 : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 =>
                    match x1 with
                    | #(idc1)%expr_pat =>
                        match
                          match idc1 with
                          | @ident.Literal t2 v =>
                              match
                                t2 as t3
                                return (base.base_interp t3 -> option Z)
                              with
                              | base.type.unit => fun _ : unit => None
                              | base.type.Z => fun v0 : Z => Some v0
                              | base.type.bool => fun _ : bool => None
                              | base.type.nat => fun _ : nat => None
                              end v
                          | _ => None
                          end
                        with
                        | Some args1 =>
                            match x2 with
                            | #(idc2)%expr_pat =>
                                match
                                  match idc2 with
                                  | @ident.Literal t3 v =>
                                      match
                                        t3 as t4
                                        return
                                          (base.base_interp t4 -> option Z)
                                      with
                                      | base.type.unit =>
                                          fun _ : unit => None
                                      | base.type.Z => fun v0 : Z => Some v0
                                      | base.type.bool =>
                                          fun _ : bool => None
                                      | base.type.nat => fun _ : nat => None
                                      end v
                                  | _ => None
                                  end
                                with
                                | Some args2 =>
                                    UnderLets.Base
                                      ##(Definitions.Z.rshi args args0 args1
                                           args2)%expr
                                | None =>
                                    UnderLets.Base
                                      (#(ident.Z_rshi)%expr @ x @ x0 @ x1 @
                                       x2)%expr_pat
                                end
                            | _ =>
                                UnderLets.Base
                                  (#(ident.Z_rshi)%expr @ x @ x0 @ x1 @ x2)%expr_pat
                            end
                        | None =>
                            UnderLets.Base
                              (#(ident.Z_rshi)%expr @ x @ x0 @ x1 @ x2)%expr_pat
                        end
                    | _ =>
                        UnderLets.Base
                          (#(ident.Z_rshi)%expr @ x @ x0 @ x1 @ x2)%expr_pat
                    end
                | None =>
                    UnderLets.Base
                      (#(ident.Z_rshi)%expr @ x @ x0 @ x1 @ x2)%expr_pat
                end
            | _ =>
                UnderLets.Base
                  (#(ident.Z_rshi)%expr @ x @ x0 @ x1 @ x2)%expr_pat
            end
        | None =>
            UnderLets.Base (#(ident.Z_rshi)%expr @ x @ x0 @ x1 @ x2)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.Z_rshi)%expr @ x @ x0 @ x1 @ x2)%expr_pat
    end
| ident.Z_cc_m =>
    fun x x0 : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args =>
            match x0 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 =>
                    UnderLets.Base ##(Definitions.Z.cc_m args args0)%expr
                | None =>
                    UnderLets.Base (#(ident.Z_cc_m)%expr @ x @ x0)%expr_pat
                end
            | _ => UnderLets.Base (#(ident.Z_cc_m)%expr @ x @ x0)%expr_pat
            end
        | None => UnderLets.Base (#(ident.Z_cc_m)%expr @ x @ x0)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.Z_cc_m)%expr @ x @ x0)%expr_pat
    end
| ident.Z_cast range =>
    fun x : defaults.expr (type.base base.type.Z) =>
    match x with
    | #(idc)%expr_pat =>
        match
          match idc with
          | @ident.Literal t0 v =>
              match t0 as t1 return (base.base_interp t1 -> option Z) with
              | base.type.unit => fun _ : unit => None
              | base.type.Z => fun v0 : Z => Some v0
              | base.type.bool => fun _ : bool => None
              | base.type.nat => fun _ : nat => None
              end v
          | _ => None
          end
        with
        | Some args =>
            UnderLets.Base
              ##(ident.cast ident.cast_outside_of_range range args)%expr
        | None => UnderLets.Base (#(ident.Z_cast range)%expr @ x)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.Z_cast range)%expr @ x)%expr_pat
    end
| ident.Z_cast2 range =>
    fun x : defaults.expr (type.base (base.type.Z * base.type.Z)%etype) =>
    match x with
    | (#(idc) @ x1 @ x0)%expr_pat =>
        match
          match idc with
          | @ident.pair A B => Some (A, B)
          | _ => None
          end
        with
        | Some _ =>
            match x1 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 =>
                    match x0 with
                    | #(idc1)%expr_pat =>
                        match
                          match idc1 with
                          | @ident.Literal t2 v =>
                              match
                                t2 as t3
                                return (base.base_interp t3 -> option Z)
                              with
                              | base.type.unit => fun _ : unit => None
                              | base.type.Z => fun v0 : Z => Some v0
                              | base.type.bool => fun _ : bool => None
                              | base.type.nat => fun _ : nat => None
                              end v
                          | _ => None
                          end
                        with
                        | Some args1 =>
                            UnderLets.Base
                              (let
                               '(a, b) :=
                                (let (r1, r2) := range in
                                 fun '(x2, x3) =>
                                 (ident.cast ident.cast_outside_of_range r1
                                    x2,
                                 ident.cast ident.cast_outside_of_range r2 x3))
                                  (args0, args1) in
                                (##(a)%expr, ##(b)%expr)%expr_pat)
                        | None =>
                            UnderLets.Base
                              (#(ident.Z_cast2 range)%expr @ x)%expr_pat
                        end
                    | _ =>
                        UnderLets.Base
                          (#(ident.Z_cast2 range)%expr @ x)%expr_pat
                    end
                | None =>
                    UnderLets.Base (#(ident.Z_cast2 range)%expr @ x)%expr_pat
                end
            | _ => UnderLets.Base (#(ident.Z_cast2 range)%expr @ x)%expr_pat
            end
        | None => UnderLets.Base (#(ident.Z_cast2 range)%expr @ x)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.Z_cast2 range)%expr @ x)%expr_pat
    end
| ident.fancy_add log2wordmax imm =>
    fun x : defaults.expr (type.base (base.type.Z * base.type.Z)%etype) =>
    match x with
    | (#(idc) @ x1 @ x0)%expr_pat =>
        match
          match idc with
          | @ident.pair A B => Some (A, B)
          | _ => None
          end
        with
        | Some _ =>
            match x1 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 =>
                    match x0 with
                    | #(idc1)%expr_pat =>
                        match
                          match idc1 with
                          | @ident.Literal t2 v =>
                              match
                                t2 as t3
                                return (base.base_interp t3 -> option Z)
                              with
                              | base.type.unit => fun _ : unit => None
                              | base.type.Z => fun v0 : Z => Some v0
                              | base.type.bool => fun _ : bool => None
                              | base.type.nat => fun _ : nat => None
                              end v
                          | _ => None
                          end
                        with
                        | Some args1 =>
                            UnderLets.Base
                              (let
                               '(a, b) :=
                                ident.fancy.interp
                                  (invert_Some
                                     (ident.to_fancy
                                        (ident.fancy_add log2wordmax imm)))
                                  (args0, args1) in
                                (##(a)%expr, ##(b)%expr)%expr_pat)
                        | None =>
                            UnderLets.Base
                              (#(ident.fancy_add log2wordmax imm)%expr @ x)%expr_pat
                        end
                    | _ =>
                        UnderLets.Base
                          (#(ident.fancy_add log2wordmax imm)%expr @ x)%expr_pat
                    end
                | None =>
                    UnderLets.Base
                      (#(ident.fancy_add log2wordmax imm)%expr @ x)%expr_pat
                end
            | _ =>
                UnderLets.Base
                  (#(ident.fancy_add log2wordmax imm)%expr @ x)%expr_pat
            end
        | None =>
            UnderLets.Base
              (#(ident.fancy_add log2wordmax imm)%expr @ x)%expr_pat
        end
    | _ =>
        UnderLets.Base (#(ident.fancy_add log2wordmax imm)%expr @ x)%expr_pat
    end
| ident.fancy_addc log2wordmax imm =>
    fun
      x : defaults.expr
            (type.base (base.type.Z * base.type.Z * base.type.Z)%etype) =>
    match x with
    | (#(idc) @ x1 @ x0)%expr_pat =>
        match
          match idc with
          | @ident.pair A B => Some (A, B)
          | _ => None
          end
        with
        | Some _ =>
            match x1 with
            | (#(idc0) @ x3 @ x2)%expr_pat =>
                match
                  match idc0 with
                  | @ident.pair A B => Some (A, B)
                  | _ => None
                  end
                with
                | Some _ =>
                    match x3 with
                    | #(idc1)%expr_pat =>
                        match
                          match idc1 with
                          | @ident.Literal t2 v =>
                              match
                                t2 as t3
                                return (base.base_interp t3 -> option Z)
                              with
                              | base.type.unit => fun _ : unit => None
                              | base.type.Z => fun v0 : Z => Some v0
                              | base.type.bool => fun _ : bool => None
                              | base.type.nat => fun _ : nat => None
                              end v
                          | _ => None
                          end
                        with
                        | Some args1 =>
                            match x2 with
                            | #(idc2)%expr_pat =>
                                match
                                  match idc2 with
                                  | @ident.Literal t3 v =>
                                      match
                                        t3 as t4
                                        return
                                          (base.base_interp t4 -> option Z)
                                      with
                                      | base.type.unit =>
                                          fun _ : unit => None
                                      | base.type.Z => fun v0 : Z => Some v0
                                      | base.type.bool =>
                                          fun _ : bool => None
                                      | base.type.nat => fun _ : nat => None
                                      end v
                                  | _ => None
                                  end
                                with
                                | Some args2 =>
                                    match x0 with
                                    | #(idc3)%expr_pat =>
                                        match
                                          match idc3 with
                                          | @ident.Literal t4 v =>
                                              match
                                                t4 as t5
                                                return
                                                  (base.base_interp t5 ->
                                                   option Z)
                                              with
                                              | base.type.unit =>
                                                  fun _ : unit => None
                                              | base.type.Z =>
                                                  fun v0 : Z => Some v0
                                              | base.type.bool =>
                                                  fun _ : bool => None
                                              | base.type.nat =>
                                                  fun _ : nat => None
                                              end v
                                          | _ => None
                                          end
                                        with
                                        | Some args3 =>
                                            UnderLets.Base
                                              (let
                                               '(a, b) :=
                                                ident.fancy.interp
                                                  (invert_Some
                                                     (ident.to_fancy
                                                        (ident.fancy_addc
                                                           log2wordmax imm)))
                                                  (args1, args2, args3) in
                                                (##(a)%expr, ##(b)%expr)%expr_pat)
                                        | None =>
                                            UnderLets.Base
                                              (#(ident.fancy_addc log2wordmax
                                                   imm)%expr @ x)%expr_pat
                                        end
                                    | _ =>
                                        UnderLets.Base
                                          (#(ident.fancy_addc log2wordmax imm)%expr @
                                           x)%expr_pat
                                    end
                                | None =>
                                    UnderLets.Base
                                      (#(ident.fancy_addc log2wordmax imm)%expr @
                                       x)%expr_pat
                                end
                            | _ =>
                                UnderLets.Base
                                  (#(ident.fancy_addc log2wordmax imm)%expr @
                                   x)%expr_pat
                            end
                        | None =>
                            UnderLets.Base
                              (#(ident.fancy_addc log2wordmax imm)%expr @ x)%expr_pat
                        end
                    | _ =>
                        UnderLets.Base
                          (#(ident.fancy_addc log2wordmax imm)%expr @ x)%expr_pat
                    end
                | None =>
                    UnderLets.Base
                      (#(ident.fancy_addc log2wordmax imm)%expr @ x)%expr_pat
                end
            | _ =>
                UnderLets.Base
                  (#(ident.fancy_addc log2wordmax imm)%expr @ x)%expr_pat
            end
        | None =>
            UnderLets.Base
              (#(ident.fancy_addc log2wordmax imm)%expr @ x)%expr_pat
        end
    | _ =>
        UnderLets.Base
          (#(ident.fancy_addc log2wordmax imm)%expr @ x)%expr_pat
    end
| ident.fancy_sub log2wordmax imm =>
    fun x : defaults.expr (type.base (base.type.Z * base.type.Z)%etype) =>
    match x with
    | (#(idc) @ x1 @ x0)%expr_pat =>
        match
          match idc with
          | @ident.pair A B => Some (A, B)
          | _ => None
          end
        with
        | Some _ =>
            match x1 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 =>
                    match x0 with
                    | #(idc1)%expr_pat =>
                        match
                          match idc1 with
                          | @ident.Literal t2 v =>
                              match
                                t2 as t3
                                return (base.base_interp t3 -> option Z)
                              with
                              | base.type.unit => fun _ : unit => None
                              | base.type.Z => fun v0 : Z => Some v0
                              | base.type.bool => fun _ : bool => None
                              | base.type.nat => fun _ : nat => None
                              end v
                          | _ => None
                          end
                        with
                        | Some args1 =>
                            UnderLets.Base
                              (let
                               '(a, b) :=
                                ident.fancy.interp
                                  (invert_Some
                                     (ident.to_fancy
                                        (ident.fancy_sub log2wordmax imm)))
                                  (args0, args1) in
                                (##(a)%expr, ##(b)%expr)%expr_pat)
                        | None =>
                            UnderLets.Base
                              (#(ident.fancy_sub log2wordmax imm)%expr @ x)%expr_pat
                        end
                    | _ =>
                        UnderLets.Base
                          (#(ident.fancy_sub log2wordmax imm)%expr @ x)%expr_pat
                    end
                | None =>
                    UnderLets.Base
                      (#(ident.fancy_sub log2wordmax imm)%expr @ x)%expr_pat
                end
            | _ =>
                UnderLets.Base
                  (#(ident.fancy_sub log2wordmax imm)%expr @ x)%expr_pat
            end
        | None =>
            UnderLets.Base
              (#(ident.fancy_sub log2wordmax imm)%expr @ x)%expr_pat
        end
    | _ =>
        UnderLets.Base (#(ident.fancy_sub log2wordmax imm)%expr @ x)%expr_pat
    end
| ident.fancy_subb log2wordmax imm =>
    fun
      x : defaults.expr
            (type.base (base.type.Z * base.type.Z * base.type.Z)%etype) =>
    match x with
    | (#(idc) @ x1 @ x0)%expr_pat =>
        match
          match idc with
          | @ident.pair A B => Some (A, B)
          | _ => None
          end
        with
        | Some _ =>
            match x1 with
            | (#(idc0) @ x3 @ x2)%expr_pat =>
                match
                  match idc0 with
                  | @ident.pair A B => Some (A, B)
                  | _ => None
                  end
                with
                | Some _ =>
                    match x3 with
                    | #(idc1)%expr_pat =>
                        match
                          match idc1 with
                          | @ident.Literal t2 v =>
                              match
                                t2 as t3
                                return (base.base_interp t3 -> option Z)
                              with
                              | base.type.unit => fun _ : unit => None
                              | base.type.Z => fun v0 : Z => Some v0
                              | base.type.bool => fun _ : bool => None
                              | base.type.nat => fun _ : nat => None
                              end v
                          | _ => None
                          end
                        with
                        | Some args1 =>
                            match x2 with
                            | #(idc2)%expr_pat =>
                                match
                                  match idc2 with
                                  | @ident.Literal t3 v =>
                                      match
                                        t3 as t4
                                        return
                                          (base.base_interp t4 -> option Z)
                                      with
                                      | base.type.unit =>
                                          fun _ : unit => None
                                      | base.type.Z => fun v0 : Z => Some v0
                                      | base.type.bool =>
                                          fun _ : bool => None
                                      | base.type.nat => fun _ : nat => None
                                      end v
                                  | _ => None
                                  end
                                with
                                | Some args2 =>
                                    match x0 with
                                    | #(idc3)%expr_pat =>
                                        match
                                          match idc3 with
                                          | @ident.Literal t4 v =>
                                              match
                                                t4 as t5
                                                return
                                                  (base.base_interp t5 ->
                                                   option Z)
                                              with
                                              | base.type.unit =>
                                                  fun _ : unit => None
                                              | base.type.Z =>
                                                  fun v0 : Z => Some v0
                                              | base.type.bool =>
                                                  fun _ : bool => None
                                              | base.type.nat =>
                                                  fun _ : nat => None
                                              end v
                                          | _ => None
                                          end
                                        with
                                        | Some args3 =>
                                            UnderLets.Base
                                              (let
                                               '(a, b) :=
                                                ident.fancy.interp
                                                  (invert_Some
                                                     (ident.to_fancy
                                                        (ident.fancy_subb
                                                           log2wordmax imm)))
                                                  (args1, args2, args3) in
                                                (##(a)%expr, ##(b)%expr)%expr_pat)
                                        | None =>
                                            UnderLets.Base
                                              (#(ident.fancy_subb log2wordmax
                                                   imm)%expr @ x)%expr_pat
                                        end
                                    | _ =>
                                        UnderLets.Base
                                          (#(ident.fancy_subb log2wordmax imm)%expr @
                                           x)%expr_pat
                                    end
                                | None =>
                                    UnderLets.Base
                                      (#(ident.fancy_subb log2wordmax imm)%expr @
                                       x)%expr_pat
                                end
                            | _ =>
                                UnderLets.Base
                                  (#(ident.fancy_subb log2wordmax imm)%expr @
                                   x)%expr_pat
                            end
                        | None =>
                            UnderLets.Base
                              (#(ident.fancy_subb log2wordmax imm)%expr @ x)%expr_pat
                        end
                    | _ =>
                        UnderLets.Base
                          (#(ident.fancy_subb log2wordmax imm)%expr @ x)%expr_pat
                    end
                | None =>
                    UnderLets.Base
                      (#(ident.fancy_subb log2wordmax imm)%expr @ x)%expr_pat
                end
            | _ =>
                UnderLets.Base
                  (#(ident.fancy_subb log2wordmax imm)%expr @ x)%expr_pat
            end
        | None =>
            UnderLets.Base
              (#(ident.fancy_subb log2wordmax imm)%expr @ x)%expr_pat
        end
    | _ =>
        UnderLets.Base
          (#(ident.fancy_subb log2wordmax imm)%expr @ x)%expr_pat
    end
| ident.fancy_mulll log2wordmax =>
    fun x : defaults.expr (type.base (base.type.Z * base.type.Z)%etype) =>
    match x with
    | (#(idc) @ x1 @ x0)%expr_pat =>
        match
          match idc with
          | @ident.pair A B => Some (A, B)
          | _ => None
          end
        with
        | Some _ =>
            match x1 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 =>
                    match x0 with
                    | #(idc1)%expr_pat =>
                        match
                          match idc1 with
                          | @ident.Literal t2 v =>
                              match
                                t2 as t3
                                return (base.base_interp t3 -> option Z)
                              with
                              | base.type.unit => fun _ : unit => None
                              | base.type.Z => fun v0 : Z => Some v0
                              | base.type.bool => fun _ : bool => None
                              | base.type.nat => fun _ : nat => None
                              end v
                          | _ => None
                          end
                        with
                        | Some args1 =>
                            UnderLets.Base
                              ##(ident.fancy.interp
                                   (invert_Some
                                      (ident.to_fancy
                                         (ident.fancy_mulll log2wordmax)))
                                   (args0, args1)%core)%expr
                        | None =>
                            UnderLets.Base
                              (#(ident.fancy_mulll log2wordmax)%expr @ x)%expr_pat
                        end
                    | _ =>
                        UnderLets.Base
                          (#(ident.fancy_mulll log2wordmax)%expr @ x)%expr_pat
                    end
                | None =>
                    UnderLets.Base
                      (#(ident.fancy_mulll log2wordmax)%expr @ x)%expr_pat
                end
            | _ =>
                UnderLets.Base
                  (#(ident.fancy_mulll log2wordmax)%expr @ x)%expr_pat
            end
        | None =>
            UnderLets.Base
              (#(ident.fancy_mulll log2wordmax)%expr @ x)%expr_pat
        end
    | _ =>
        UnderLets.Base (#(ident.fancy_mulll log2wordmax)%expr @ x)%expr_pat
    end
| ident.fancy_mullh log2wordmax =>
    fun x : defaults.expr (type.base (base.type.Z * base.type.Z)%etype) =>
    match x with
    | (#(idc) @ x1 @ x0)%expr_pat =>
        match
          match idc with
          | @ident.pair A B => Some (A, B)
          | _ => None
          end
        with
        | Some _ =>
            match x1 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 =>
                    match x0 with
                    | #(idc1)%expr_pat =>
                        match
                          match idc1 with
                          | @ident.Literal t2 v =>
                              match
                                t2 as t3
                                return (base.base_interp t3 -> option Z)
                              with
                              | base.type.unit => fun _ : unit => None
                              | base.type.Z => fun v0 : Z => Some v0
                              | base.type.bool => fun _ : bool => None
                              | base.type.nat => fun _ : nat => None
                              end v
                          | _ => None
                          end
                        with
                        | Some args1 =>
                            UnderLets.Base
                              ##(ident.fancy.interp
                                   (invert_Some
                                      (ident.to_fancy
                                         (ident.fancy_mullh log2wordmax)))
                                   (args0, args1)%core)%expr
                        | None =>
                            UnderLets.Base
                              (#(ident.fancy_mullh log2wordmax)%expr @ x)%expr_pat
                        end
                    | _ =>
                        UnderLets.Base
                          (#(ident.fancy_mullh log2wordmax)%expr @ x)%expr_pat
                    end
                | None =>
                    UnderLets.Base
                      (#(ident.fancy_mullh log2wordmax)%expr @ x)%expr_pat
                end
            | _ =>
                UnderLets.Base
                  (#(ident.fancy_mullh log2wordmax)%expr @ x)%expr_pat
            end
        | None =>
            UnderLets.Base
              (#(ident.fancy_mullh log2wordmax)%expr @ x)%expr_pat
        end
    | _ =>
        UnderLets.Base (#(ident.fancy_mullh log2wordmax)%expr @ x)%expr_pat
    end
| ident.fancy_mulhl log2wordmax =>
    fun x : defaults.expr (type.base (base.type.Z * base.type.Z)%etype) =>
    match x with
    | (#(idc) @ x1 @ x0)%expr_pat =>
        match
          match idc with
          | @ident.pair A B => Some (A, B)
          | _ => None
          end
        with
        | Some _ =>
            match x1 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 =>
                    match x0 with
                    | #(idc1)%expr_pat =>
                        match
                          match idc1 with
                          | @ident.Literal t2 v =>
                              match
                                t2 as t3
                                return (base.base_interp t3 -> option Z)
                              with
                              | base.type.unit => fun _ : unit => None
                              | base.type.Z => fun v0 : Z => Some v0
                              | base.type.bool => fun _ : bool => None
                              | base.type.nat => fun _ : nat => None
                              end v
                          | _ => None
                          end
                        with
                        | Some args1 =>
                            UnderLets.Base
                              ##(ident.fancy.interp
                                   (invert_Some
                                      (ident.to_fancy
                                         (ident.fancy_mulhl log2wordmax)))
                                   (args0, args1)%core)%expr
                        | None =>
                            UnderLets.Base
                              (#(ident.fancy_mulhl log2wordmax)%expr @ x)%expr_pat
                        end
                    | _ =>
                        UnderLets.Base
                          (#(ident.fancy_mulhl log2wordmax)%expr @ x)%expr_pat
                    end
                | None =>
                    UnderLets.Base
                      (#(ident.fancy_mulhl log2wordmax)%expr @ x)%expr_pat
                end
            | _ =>
                UnderLets.Base
                  (#(ident.fancy_mulhl log2wordmax)%expr @ x)%expr_pat
            end
        | None =>
            UnderLets.Base
              (#(ident.fancy_mulhl log2wordmax)%expr @ x)%expr_pat
        end
    | _ =>
        UnderLets.Base (#(ident.fancy_mulhl log2wordmax)%expr @ x)%expr_pat
    end
| ident.fancy_mulhh log2wordmax =>
    fun x : defaults.expr (type.base (base.type.Z * base.type.Z)%etype) =>
    match x with
    | (#(idc) @ x1 @ x0)%expr_pat =>
        match
          match idc with
          | @ident.pair A B => Some (A, B)
          | _ => None
          end
        with
        | Some _ =>
            match x1 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 =>
                    match x0 with
                    | #(idc1)%expr_pat =>
                        match
                          match idc1 with
                          | @ident.Literal t2 v =>
                              match
                                t2 as t3
                                return (base.base_interp t3 -> option Z)
                              with
                              | base.type.unit => fun _ : unit => None
                              | base.type.Z => fun v0 : Z => Some v0
                              | base.type.bool => fun _ : bool => None
                              | base.type.nat => fun _ : nat => None
                              end v
                          | _ => None
                          end
                        with
                        | Some args1 =>
                            UnderLets.Base
                              ##(ident.fancy.interp
                                   (invert_Some
                                      (ident.to_fancy
                                         (ident.fancy_mulhh log2wordmax)))
                                   (args0, args1)%core)%expr
                        | None =>
                            UnderLets.Base
                              (#(ident.fancy_mulhh log2wordmax)%expr @ x)%expr_pat
                        end
                    | _ =>
                        UnderLets.Base
                          (#(ident.fancy_mulhh log2wordmax)%expr @ x)%expr_pat
                    end
                | None =>
                    UnderLets.Base
                      (#(ident.fancy_mulhh log2wordmax)%expr @ x)%expr_pat
                end
            | _ =>
                UnderLets.Base
                  (#(ident.fancy_mulhh log2wordmax)%expr @ x)%expr_pat
            end
        | None =>
            UnderLets.Base
              (#(ident.fancy_mulhh log2wordmax)%expr @ x)%expr_pat
        end
    | _ =>
        UnderLets.Base (#(ident.fancy_mulhh log2wordmax)%expr @ x)%expr_pat
    end
| ident.fancy_rshi log2wordmax x =>
    fun x0 : defaults.expr (type.base (base.type.Z * base.type.Z)%etype) =>
    match x0 with
    | (#(idc) @ x2 @ x1)%expr_pat =>
        match
          match idc with
          | @ident.pair A B => Some (A, B)
          | _ => None
          end
        with
        | Some _ =>
            match x2 with
            | #(idc0)%expr_pat =>
                match
                  match idc0 with
                  | @ident.Literal t1 v =>
                      match
                        t1 as t2 return (base.base_interp t2 -> option Z)
                      with
                      | base.type.unit => fun _ : unit => None
                      | base.type.Z => fun v0 : Z => Some v0
                      | base.type.bool => fun _ : bool => None
                      | base.type.nat => fun _ : nat => None
                      end v
                  | _ => None
                  end
                with
                | Some args0 =>
                    match x1 with
                    | #(idc1)%expr_pat =>
                        match
                          match idc1 with
                          | @ident.Literal t2 v =>
                              match
                                t2 as t3
                                return (base.base_interp t3 -> option Z)
                              with
                              | base.type.unit => fun _ : unit => None
                              | base.type.Z => fun v0 : Z => Some v0
                              | base.type.bool => fun _ : bool => None
                              | base.type.nat => fun _ : nat => None
                              end v
                          | _ => None
                          end
                        with
                        | Some args1 =>
                            UnderLets.Base
                              ##(ident.fancy.interp
                                   (invert_Some
                                      (ident.to_fancy
                                         (ident.fancy_rshi log2wordmax x)))
                                   (args0, args1)%core)%expr
                        | None =>
                            UnderLets.Base
                              (#(ident.fancy_rshi log2wordmax x)%expr @ x0)%expr_pat
                        end
                    | _ =>
                        UnderLets.Base
                          (#(ident.fancy_rshi log2wordmax x)%expr @ x0)%expr_pat
                    end
                | None =>
                    UnderLets.Base
                      (#(ident.fancy_rshi log2wordmax x)%expr @ x0)%expr_pat
                end
            | _ =>
                UnderLets.Base
                  (#(ident.fancy_rshi log2wordmax x)%expr @ x0)%expr_pat
            end
        | None =>
            UnderLets.Base
              (#(ident.fancy_rshi log2wordmax x)%expr @ x0)%expr_pat
        end
    | _ =>
        UnderLets.Base (#(ident.fancy_rshi log2wordmax x)%expr @ x0)%expr_pat
    end
| ident.fancy_selc =>
    fun
      x : defaults.expr
            (type.base (base.type.Z * base.type.Z * base.type.Z)%etype) =>
    match x with
    | (#(idc) @ x1 @ x0)%expr_pat =>
        match
          match idc with
          | @ident.pair A B => Some (A, B)
          | _ => None
          end
        with
        | Some _ =>
            match x1 with
            | (#(idc0) @ x3 @ x2)%expr_pat =>
                match
                  match idc0 with
                  | @ident.pair A B => Some (A, B)
                  | _ => None
                  end
                with
                | Some _ =>
                    match x3 with
                    | #(idc1)%expr_pat =>
                        match
                          match idc1 with
                          | @ident.Literal t2 v =>
                              match
                                t2 as t3
                                return (base.base_interp t3 -> option Z)
                              with
                              | base.type.unit => fun _ : unit => None
                              | base.type.Z => fun v0 : Z => Some v0
                              | base.type.bool => fun _ : bool => None
                              | base.type.nat => fun _ : nat => None
                              end v
                          | _ => None
                          end
                        with
                        | Some args1 =>
                            match x2 with
                            | #(idc2)%expr_pat =>
                                match
                                  match idc2 with
                                  | @ident.Literal t3 v =>
                                      match
                                        t3 as t4
                                        return
                                          (base.base_interp t4 -> option Z)
                                      with
                                      | base.type.unit =>
                                          fun _ : unit => None
                                      | base.type.Z => fun v0 : Z => Some v0
                                      | base.type.bool =>
                                          fun _ : bool => None
                                      | base.type.nat => fun _ : nat => None
                                      end v
                                  | _ => None
                                  end
                                with
                                | Some args2 =>
                                    match x0 with
                                    | #(idc3)%expr_pat =>
                                        match
                                          match idc3 with
                                          | @ident.Literal t4 v =>
                                              match
                                                t4 as t5
                                                return
                                                  (base.base_interp t5 ->
                                                   option Z)
                                              with
                                              | base.type.unit =>
                                                  fun _ : unit => None
                                              | base.type.Z =>
                                                  fun v0 : Z => Some v0
                                              | base.type.bool =>
                                                  fun _ : bool => None
                                              | base.type.nat =>
                                                  fun _ : nat => None
                                              end v
                                          | _ => None
                                          end
                                        with
                                        | Some args3 =>
                                            UnderLets.Base
                                              ##(ident.fancy.interp
                                                   (invert_Some
                                                      (ident.to_fancy
                                                         ident.fancy_selc))
                                                   (args1, args2, args3)%core)%expr
                                        | None =>
                                            UnderLets.Base
                                              (#(ident.fancy_selc)%expr @ x)%expr_pat
                                        end
                                    | _ =>
                                        UnderLets.Base
                                          (#(ident.fancy_selc)%expr @ x)%expr_pat
                                    end
                                | None =>
                                    UnderLets.Base
                                      (#(ident.fancy_selc)%expr @ x)%expr_pat
                                end
                            | _ =>
                                UnderLets.Base
                                  (#(ident.fancy_selc)%expr @ x)%expr_pat
                            end
                        | None =>
                            UnderLets.Base
                              (#(ident.fancy_selc)%expr @ x)%expr_pat
                        end
                    | _ =>
                        UnderLets.Base
                          (#(ident.fancy_selc)%expr @ x)%expr_pat
                    end
                | None =>
                    UnderLets.Base (#(ident.fancy_selc)%expr @ x)%expr_pat
                end
            | _ => UnderLets.Base (#(ident.fancy_selc)%expr @ x)%expr_pat
            end
        | None => UnderLets.Base (#(ident.fancy_selc)%expr @ x)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.fancy_selc)%expr @ x)%expr_pat
    end
| ident.fancy_selm log2wordmax =>
    fun
      x : defaults.expr
            (type.base (base.type.Z * base.type.Z * base.type.Z)%etype) =>
    match x with
    | (#(idc) @ x1 @ x0)%expr_pat =>
        match
          match idc with
          | @ident.pair A B => Some (A, B)
          | _ => None
          end
        with
        | Some _ =>
            match x1 with
            | (#(idc0) @ x3 @ x2)%expr_pat =>
                match
                  match idc0 with
                  | @ident.pair A B => Some (A, B)
                  | _ => None
                  end
                with
                | Some _ =>
                    match x3 with
                    | #(idc1)%expr_pat =>
                        match
                          match idc1 with
                          | @ident.Literal t2 v =>
                              match
                                t2 as t3
                                return (base.base_interp t3 -> option Z)
                              with
                              | base.type.unit => fun _ : unit => None
                              | base.type.Z => fun v0 : Z => Some v0
                              | base.type.bool => fun _ : bool => None
                              | base.type.nat => fun _ : nat => None
                              end v
                          | _ => None
                          end
                        with
                        | Some args1 =>
                            match x2 with
                            | #(idc2)%expr_pat =>
                                match
                                  match idc2 with
                                  | @ident.Literal t3 v =>
                                      match
                                        t3 as t4
                                        return
                                          (base.base_interp t4 -> option Z)
                                      with
                                      | base.type.unit =>
                                          fun _ : unit => None
                                      | base.type.Z => fun v0 : Z => Some v0
                                      | base.type.bool =>
                                          fun _ : bool => None
                                      | base.type.nat => fun _ : nat => None
                                      end v
                                  | _ => None
                                  end
                                with
                                | Some args2 =>
                                    match x0 with
                                    | #(idc3)%expr_pat =>
                                        match
                                          match idc3 with
                                          | @ident.Literal t4 v =>
                                              match
                                                t4 as t5
                                                return
                                                  (base.base_interp t5 ->
                                                   option Z)
                                              with
                                              | base.type.unit =>
                                                  fun _ : unit => None
                                              | base.type.Z =>
                                                  fun v0 : Z => Some v0
                                              | base.type.bool =>
                                                  fun _ : bool => None
                                              | base.type.nat =>
                                                  fun _ : nat => None
                                              end v
                                          | _ => None
                                          end
                                        with
                                        | Some args3 =>
                                            UnderLets.Base
                                              ##(ident.fancy.interp
                                                   (invert_Some
                                                      (ident.to_fancy
                                                         (ident.fancy_selm
                                                            log2wordmax)))
                                                   (args1, args2, args3)%core)%expr
                                        | None =>
                                            UnderLets.Base
                                              (#(ident.fancy_selm log2wordmax)%expr @
                                               x)%expr_pat
                                        end
                                    | _ =>
                                        UnderLets.Base
                                          (#(ident.fancy_selm log2wordmax)%expr @
                                           x)%expr_pat
                                    end
                                | None =>
                                    UnderLets.Base
                                      (#(ident.fancy_selm log2wordmax)%expr @
                                       x)%expr_pat
                                end
                            | _ =>
                                UnderLets.Base
                                  (#(ident.fancy_selm log2wordmax)%expr @ x)%expr_pat
                            end
                        | None =>
                            UnderLets.Base
                              (#(ident.fancy_selm log2wordmax)%expr @ x)%expr_pat
                        end
                    | _ =>
                        UnderLets.Base
                          (#(ident.fancy_selm log2wordmax)%expr @ x)%expr_pat
                    end
                | None =>
                    UnderLets.Base
                      (#(ident.fancy_selm log2wordmax)%expr @ x)%expr_pat
                end
            | _ =>
                UnderLets.Base
                  (#(ident.fancy_selm log2wordmax)%expr @ x)%expr_pat
            end
        | None =>
            UnderLets.Base
              (#(ident.fancy_selm log2wordmax)%expr @ x)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.fancy_selm log2wordmax)%expr @ x)%expr_pat
    end
| ident.fancy_sell =>
    fun
      x : defaults.expr
            (type.base (base.type.Z * base.type.Z * base.type.Z)%etype) =>
    match x with
    | (#(idc) @ x1 @ x0)%expr_pat =>
        match
          match idc with
          | @ident.pair A B => Some (A, B)
          | _ => None
          end
        with
        | Some _ =>
            match x1 with
            | (#(idc0) @ x3 @ x2)%expr_pat =>
                match
                  match idc0 with
                  | @ident.pair A B => Some (A, B)
                  | _ => None
                  end
                with
                | Some _ =>
                    match x3 with
                    | #(idc1)%expr_pat =>
                        match
                          match idc1 with
                          | @ident.Literal t2 v =>
                              match
                                t2 as t3
                                return (base.base_interp t3 -> option Z)
                              with
                              | base.type.unit => fun _ : unit => None
                              | base.type.Z => fun v0 : Z => Some v0
                              | base.type.bool => fun _ : bool => None
                              | base.type.nat => fun _ : nat => None
                              end v
                          | _ => None
                          end
                        with
                        | Some args1 =>
                            match x2 with
                            | #(idc2)%expr_pat =>
                                match
                                  match idc2 with
                                  | @ident.Literal t3 v =>
                                      match
                                        t3 as t4
                                        return
                                          (base.base_interp t4 -> option Z)
                                      with
                                      | base.type.unit =>
                                          fun _ : unit => None
                                      | base.type.Z => fun v0 : Z => Some v0
                                      | base.type.bool =>
                                          fun _ : bool => None
                                      | base.type.nat => fun _ : nat => None
                                      end v
                                  | _ => None
                                  end
                                with
                                | Some args2 =>
                                    match x0 with
                                    | #(idc3)%expr_pat =>
                                        match
                                          match idc3 with
                                          | @ident.Literal t4 v =>
                                              match
                                                t4 as t5
                                                return
                                                  (base.base_interp t5 ->
                                                   option Z)
                                              with
                                              | base.type.unit =>
                                                  fun _ : unit => None
                                              | base.type.Z =>
                                                  fun v0 : Z => Some v0
                                              | base.type.bool =>
                                                  fun _ : bool => None
                                              | base.type.nat =>
                                                  fun _ : nat => None
                                              end v
                                          | _ => None
                                          end
                                        with
                                        | Some args3 =>
                                            UnderLets.Base
                                              ##(ident.fancy.interp
                                                   (invert_Some
                                                      (ident.to_fancy
                                                         ident.fancy_sell))
                                                   (args1, args2, args3)%core)%expr
                                        | None =>
                                            UnderLets.Base
                                              (#(ident.fancy_sell)%expr @ x)%expr_pat
                                        end
                                    | _ =>
                                        UnderLets.Base
                                          (#(ident.fancy_sell)%expr @ x)%expr_pat
                                    end
                                | None =>
                                    UnderLets.Base
                                      (#(ident.fancy_sell)%expr @ x)%expr_pat
                                end
                            | _ =>
                                UnderLets.Base
                                  (#(ident.fancy_sell)%expr @ x)%expr_pat
                            end
                        | None =>
                            UnderLets.Base
                              (#(ident.fancy_sell)%expr @ x)%expr_pat
                        end
                    | _ =>
                        UnderLets.Base
                          (#(ident.fancy_sell)%expr @ x)%expr_pat
                    end
                | None =>
                    UnderLets.Base (#(ident.fancy_sell)%expr @ x)%expr_pat
                end
            | _ => UnderLets.Base (#(ident.fancy_sell)%expr @ x)%expr_pat
            end
        | None => UnderLets.Base (#(ident.fancy_sell)%expr @ x)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.fancy_sell)%expr @ x)%expr_pat
    end
| ident.fancy_addm =>
    fun
      x : defaults.expr
            (type.base (base.type.Z * base.type.Z * base.type.Z)%etype) =>
    match x with
    | (#(idc) @ x1 @ x0)%expr_pat =>
        match
          match idc with
          | @ident.pair A B => Some (A, B)
          | _ => None
          end
        with
        | Some _ =>
            match x1 with
            | (#(idc0) @ x3 @ x2)%expr_pat =>
                match
                  match idc0 with
                  | @ident.pair A B => Some (A, B)
                  | _ => None
                  end
                with
                | Some _ =>
                    match x3 with
                    | #(idc1)%expr_pat =>
                        match
                          match idc1 with
                          | @ident.Literal t2 v =>
                              match
                                t2 as t3
                                return (base.base_interp t3 -> option Z)
                              with
                              | base.type.unit => fun _ : unit => None
                              | base.type.Z => fun v0 : Z => Some v0
                              | base.type.bool => fun _ : bool => None
                              | base.type.nat => fun _ : nat => None
                              end v
                          | _ => None
                          end
                        with
                        | Some args1 =>
                            match x2 with
                            | #(idc2)%expr_pat =>
                                match
                                  match idc2 with
                                  | @ident.Literal t3 v =>
                                      match
                                        t3 as t4
                                        return
                                          (base.base_interp t4 -> option Z)
                                      with
                                      | base.type.unit =>
                                          fun _ : unit => None
                                      | base.type.Z => fun v0 : Z => Some v0
                                      | base.type.bool =>
                                          fun _ : bool => None
                                      | base.type.nat => fun _ : nat => None
                                      end v
                                  | _ => None
                                  end
                                with
                                | Some args2 =>
                                    match x0 with
                                    | #(idc3)%expr_pat =>
                                        match
                                          match idc3 with
                                          | @ident.Literal t4 v =>
                                              match
                                                t4 as t5
                                                return
                                                  (base.base_interp t5 ->
                                                   option Z)
                                              with
                                              | base.type.unit =>
                                                  fun _ : unit => None
                                              | base.type.Z =>
                                                  fun v0 : Z => Some v0
                                              | base.type.bool =>
                                                  fun _ : bool => None
                                              | base.type.nat =>
                                                  fun _ : nat => None
                                              end v
                                          | _ => None
                                          end
                                        with
                                        | Some args3 =>
                                            UnderLets.Base
                                              ##(ident.fancy.interp
                                                   (invert_Some
                                                      (ident.to_fancy
                                                         ident.fancy_addm))
                                                   (args1, args2, args3)%core)%expr
                                        | None =>
                                            UnderLets.Base
                                              (#(ident.fancy_addm)%expr @ x)%expr_pat
                                        end
                                    | _ =>
                                        UnderLets.Base
                                          (#(ident.fancy_addm)%expr @ x)%expr_pat
                                    end
                                | None =>
                                    UnderLets.Base
                                      (#(ident.fancy_addm)%expr @ x)%expr_pat
                                end
                            | _ =>
                                UnderLets.Base
                                  (#(ident.fancy_addm)%expr @ x)%expr_pat
                            end
                        | None =>
                            UnderLets.Base
                              (#(ident.fancy_addm)%expr @ x)%expr_pat
                        end
                    | _ =>
                        UnderLets.Base
                          (#(ident.fancy_addm)%expr @ x)%expr_pat
                    end
                | None =>
                    UnderLets.Base (#(ident.fancy_addm)%expr @ x)%expr_pat
                end
            | _ => UnderLets.Base (#(ident.fancy_addm)%expr @ x)%expr_pat
            end
        | None => UnderLets.Base (#(ident.fancy_addm)%expr @ x)%expr_pat
        end
    | _ => UnderLets.Base (#(ident.fancy_addm)%expr @ x)%expr_pat
    end
end
     : Compile.value' true t