(* Generated by coq-of-rust *)
Require Import CoqOfRust.CoqOfRust.

Module slice.
  Module index.
    Module Impl_core_ops_index_Index_where_core_slice_index_SliceIndex_I_slice_T_I_for_slice_T.
      Definition Self (T I : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ T ].
      
      (*     type Output = I::Output; *)
      Definition _Output (T I : Ty.t) : Ty.t := Ty.associated.
      
      (*
          fn index(&self, index: I) -> &I::Output {
              index.index(self)
          }
      *)
      Definition index (T I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T I in
        match ε, τ, α with
        | [], [], [ self; index ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let index := M.alloc (| index |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                I,
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "index",
                []
              |),
              [ M.read (| index |); M.read (| self |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T I : Ty.t),
        M.IsTraitInstance
          "core::ops::index::Index"
          (Self T I)
          (* Trait polymorphic types *) [ (* Idx *) I ]
          (* Instance *)
          [ ("Output", InstanceField.Ty (_Output T I)); ("index", InstanceField.Method (index T I))
          ].
    End Impl_core_ops_index_Index_where_core_slice_index_SliceIndex_I_slice_T_I_for_slice_T.
    
    Module Impl_core_ops_index_IndexMut_where_core_slice_index_SliceIndex_I_slice_T_I_for_slice_T.
      Definition Self (T I : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ T ].
      
      (*
          fn index_mut(&mut self, index: I) -> &mut I::Output {
              index.index_mut(self)
          }
      *)
      Definition index_mut (T I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T I in
        match ε, τ, α with
        | [], [], [ self; index ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let index := M.alloc (| index |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                I,
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "index_mut",
                []
              |),
              [ M.read (| index |); M.read (| self |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T I : Ty.t),
        M.IsTraitInstance
          "core::ops::index::IndexMut"
          (Self T I)
          (* Trait polymorphic types *) [ (* Idx *) I ]
          (* Instance *) [ ("index_mut", InstanceField.Method (index_mut T I)) ].
    End Impl_core_ops_index_IndexMut_where_core_slice_index_SliceIndex_I_slice_T_I_for_slice_T.
    
    (*
    const fn slice_start_index_len_fail(index: usize, len: usize) -> ! {
        // FIXME(const-hack): once integer formatting in panics is possible, we
        // should use the same implementation at compiletime and runtime.
        const_eval_select((index, len), slice_start_index_len_fail_ct, slice_start_index_len_fail_rt)
    }
    *)
    Definition slice_start_index_len_fail
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ index; len ] =>
        ltac:(M.monadic
          (let index := M.alloc (| index |) in
          let len := M.alloc (| len |) in
          M.call_closure (|
            M.get_function (|
              "core::intrinsics::const_eval_select",
              [
                Ty.tuple [ Ty.path "usize"; Ty.path "usize" ];
                Ty.function [ Ty.path "usize"; Ty.path "usize" ] (Ty.path "never");
                Ty.function [ Ty.path "usize"; Ty.path "usize" ] (Ty.path "never");
                Ty.path "never"
              ]
            |),
            [
              Value.Tuple [ M.read (| index |); M.read (| len |) ];
              M.get_function (| "core::slice::index::slice_start_index_len_fail_ct", [] |);
              M.get_function (| "core::slice::index::slice_start_index_len_fail_rt", [] |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_slice_start_index_len_fail :
      M.IsFunction "core::slice::index::slice_start_index_len_fail" slice_start_index_len_fail.
    
    (*
    fn slice_start_index_len_fail_rt(index: usize, len: usize) -> ! {
        panic!("range start index {index} out of range for slice of length {len}");
    }
    *)
    Definition slice_start_index_len_fail_rt
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ index; len ] =>
        ltac:(M.monadic
          (let index := M.alloc (| index |) in
          let len := M.alloc (| len |) in
          M.call_closure (|
            M.get_function (| "core::panicking::panic_fmt", [] |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_v1", [] |),
                [
                  M.alloc (|
                    Value.Array
                      [
                        M.read (| Value.String "range start index " |);
                        M.read (| Value.String " out of range for slice of length " |)
                      ]
                  |);
                  M.alloc (|
                    Value.Array
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::rt::Argument",
                            "new_display",
                            [ Ty.path "usize" ]
                          |),
                          [ index ]
                        |);
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::rt::Argument",
                            "new_display",
                            [ Ty.path "usize" ]
                          |),
                          [ len ]
                        |)
                      ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_slice_start_index_len_fail_rt :
      M.IsFunction
        "core::slice::index::slice_start_index_len_fail_rt"
        slice_start_index_len_fail_rt.
    
    (*
    const fn slice_start_index_len_fail_ct(_: usize, _: usize) -> ! {
        panic!("slice start index is out of range for slice");
    }
    *)
    Definition slice_start_index_len_fail_ct
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ β0; β1 ] =>
        ltac:(M.monadic
          (let β0 := M.alloc (| β0 |) in
          let β1 := M.alloc (| β1 |) in
          M.match_operator (|
            β0,
            [
              fun γ =>
                ltac:(M.monadic
                  (M.match_operator (|
                    β1,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (M.call_closure (|
                            M.get_function (| "core::panicking::panic_fmt", [] |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::Arguments",
                                  "new_const",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    Value.Array
                                      [
                                        M.read (|
                                          Value.String "slice start index is out of range for slice"
                                        |)
                                      ]
                                  |)
                                ]
                              |)
                            ]
                          |)))
                    ]
                  |)))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_slice_start_index_len_fail_ct :
      M.IsFunction
        "core::slice::index::slice_start_index_len_fail_ct"
        slice_start_index_len_fail_ct.
    
    (*
    const fn slice_end_index_len_fail(index: usize, len: usize) -> ! {
        // FIXME(const-hack): once integer formatting in panics is possible, we
        // should use the same implementation at compiletime and runtime.
        const_eval_select((index, len), slice_end_index_len_fail_ct, slice_end_index_len_fail_rt)
    }
    *)
    Definition slice_end_index_len_fail (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ index; len ] =>
        ltac:(M.monadic
          (let index := M.alloc (| index |) in
          let len := M.alloc (| len |) in
          M.call_closure (|
            M.get_function (|
              "core::intrinsics::const_eval_select",
              [
                Ty.tuple [ Ty.path "usize"; Ty.path "usize" ];
                Ty.function [ Ty.path "usize"; Ty.path "usize" ] (Ty.path "never");
                Ty.function [ Ty.path "usize"; Ty.path "usize" ] (Ty.path "never");
                Ty.path "never"
              ]
            |),
            [
              Value.Tuple [ M.read (| index |); M.read (| len |) ];
              M.get_function (| "core::slice::index::slice_end_index_len_fail_ct", [] |);
              M.get_function (| "core::slice::index::slice_end_index_len_fail_rt", [] |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_slice_end_index_len_fail :
      M.IsFunction "core::slice::index::slice_end_index_len_fail" slice_end_index_len_fail.
    
    (*
    fn slice_end_index_len_fail_rt(index: usize, len: usize) -> ! {
        panic!("range end index {index} out of range for slice of length {len}");
    }
    *)
    Definition slice_end_index_len_fail_rt
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ index; len ] =>
        ltac:(M.monadic
          (let index := M.alloc (| index |) in
          let len := M.alloc (| len |) in
          M.call_closure (|
            M.get_function (| "core::panicking::panic_fmt", [] |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_v1", [] |),
                [
                  M.alloc (|
                    Value.Array
                      [
                        M.read (| Value.String "range end index " |);
                        M.read (| Value.String " out of range for slice of length " |)
                      ]
                  |);
                  M.alloc (|
                    Value.Array
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::rt::Argument",
                            "new_display",
                            [ Ty.path "usize" ]
                          |),
                          [ index ]
                        |);
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::rt::Argument",
                            "new_display",
                            [ Ty.path "usize" ]
                          |),
                          [ len ]
                        |)
                      ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_slice_end_index_len_fail_rt :
      M.IsFunction "core::slice::index::slice_end_index_len_fail_rt" slice_end_index_len_fail_rt.
    
    (*
    const fn slice_end_index_len_fail_ct(_: usize, _: usize) -> ! {
        panic!("slice end index is out of range for slice");
    }
    *)
    Definition slice_end_index_len_fail_ct
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ β0; β1 ] =>
        ltac:(M.monadic
          (let β0 := M.alloc (| β0 |) in
          let β1 := M.alloc (| β1 |) in
          M.match_operator (|
            β0,
            [
              fun γ =>
                ltac:(M.monadic
                  (M.match_operator (|
                    β1,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (M.call_closure (|
                            M.get_function (| "core::panicking::panic_fmt", [] |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::Arguments",
                                  "new_const",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    Value.Array
                                      [
                                        M.read (|
                                          Value.String "slice end index is out of range for slice"
                                        |)
                                      ]
                                  |)
                                ]
                              |)
                            ]
                          |)))
                    ]
                  |)))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_slice_end_index_len_fail_ct :
      M.IsFunction "core::slice::index::slice_end_index_len_fail_ct" slice_end_index_len_fail_ct.
    
    (*
    const fn slice_index_order_fail(index: usize, end: usize) -> ! {
        // FIXME(const-hack): once integer formatting in panics is possible, we
        // should use the same implementation at compiletime and runtime.
        const_eval_select((index, end), slice_index_order_fail_ct, slice_index_order_fail_rt)
    }
    *)
    Definition slice_index_order_fail (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ index; end_ ] =>
        ltac:(M.monadic
          (let index := M.alloc (| index |) in
          let end_ := M.alloc (| end_ |) in
          M.call_closure (|
            M.get_function (|
              "core::intrinsics::const_eval_select",
              [
                Ty.tuple [ Ty.path "usize"; Ty.path "usize" ];
                Ty.function [ Ty.path "usize"; Ty.path "usize" ] (Ty.path "never");
                Ty.function [ Ty.path "usize"; Ty.path "usize" ] (Ty.path "never");
                Ty.path "never"
              ]
            |),
            [
              Value.Tuple [ M.read (| index |); M.read (| end_ |) ];
              M.get_function (| "core::slice::index::slice_index_order_fail_ct", [] |);
              M.get_function (| "core::slice::index::slice_index_order_fail_rt", [] |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_slice_index_order_fail :
      M.IsFunction "core::slice::index::slice_index_order_fail" slice_index_order_fail.
    
    (*
    fn slice_index_order_fail_rt(index: usize, end: usize) -> ! {
        panic!("slice index starts at {index} but ends at {end}");
    }
    *)
    Definition slice_index_order_fail_rt
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ index; end_ ] =>
        ltac:(M.monadic
          (let index := M.alloc (| index |) in
          let end_ := M.alloc (| end_ |) in
          M.call_closure (|
            M.get_function (| "core::panicking::panic_fmt", [] |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_v1", [] |),
                [
                  M.alloc (|
                    Value.Array
                      [
                        M.read (| Value.String "slice index starts at " |);
                        M.read (| Value.String " but ends at " |)
                      ]
                  |);
                  M.alloc (|
                    Value.Array
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::rt::Argument",
                            "new_display",
                            [ Ty.path "usize" ]
                          |),
                          [ index ]
                        |);
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::rt::Argument",
                            "new_display",
                            [ Ty.path "usize" ]
                          |),
                          [ end_ ]
                        |)
                      ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_slice_index_order_fail_rt :
      M.IsFunction "core::slice::index::slice_index_order_fail_rt" slice_index_order_fail_rt.
    
    (*
    const fn slice_index_order_fail_ct(_: usize, _: usize) -> ! {
        panic!("slice index start is larger than end");
    }
    *)
    Definition slice_index_order_fail_ct
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ β0; β1 ] =>
        ltac:(M.monadic
          (let β0 := M.alloc (| β0 |) in
          let β1 := M.alloc (| β1 |) in
          M.match_operator (|
            β0,
            [
              fun γ =>
                ltac:(M.monadic
                  (M.match_operator (|
                    β1,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (M.call_closure (|
                            M.get_function (| "core::panicking::panic_fmt", [] |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::Arguments",
                                  "new_const",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    Value.Array
                                      [
                                        M.read (|
                                          Value.String "slice index start is larger than end"
                                        |)
                                      ]
                                  |)
                                ]
                              |)
                            ]
                          |)))
                    ]
                  |)))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_slice_index_order_fail_ct :
      M.IsFunction "core::slice::index::slice_index_order_fail_ct" slice_index_order_fail_ct.
    
    (*
    const fn slice_start_index_overflow_fail() -> ! {
        panic!("attempted to index slice from after maximum usize");
    }
    *)
    Definition slice_start_index_overflow_fail
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (M.call_closure (|
            M.get_function (| "core::panicking::panic_fmt", [] |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_const", [] |),
                [
                  M.alloc (|
                    Value.Array
                      [
                        M.read (|
                          Value.String "attempted to index slice from after maximum usize"
                        |)
                      ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_slice_start_index_overflow_fail :
      M.IsFunction
        "core::slice::index::slice_start_index_overflow_fail"
        slice_start_index_overflow_fail.
    
    (*
    const fn slice_end_index_overflow_fail() -> ! {
        panic!("attempted to index slice up to maximum usize");
    }
    *)
    Definition slice_end_index_overflow_fail
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (M.call_closure (|
            M.get_function (| "core::panicking::panic_fmt", [] |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_const", [] |),
                [
                  M.alloc (|
                    Value.Array
                      [ M.read (| Value.String "attempted to index slice up to maximum usize" |) ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_slice_end_index_overflow_fail :
      M.IsFunction
        "core::slice::index::slice_end_index_overflow_fail"
        slice_end_index_overflow_fail.
    
    (*
    const unsafe fn get_noubcheck<T>(ptr: *const [T], index: usize) -> *const T {
        let ptr = ptr as *const T;
        // SAFETY: The caller already checked these preconditions
        unsafe { crate::intrinsics::offset(ptr, index) }
    }
    *)
    Definition get_noubcheck (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ ptr; index ] =>
        ltac:(M.monadic
          (let ptr := M.alloc (| ptr |) in
          let index := M.alloc (| index |) in
          M.read (|
            let~ ptr := M.alloc (| M.rust_cast (M.read (| ptr |)) |) in
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::offset",
                  [ Ty.apply (Ty.path "*const") [] [ T ]; Ty.path "usize" ]
                |),
                [ M.read (| ptr |); M.read (| index |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_get_noubcheck : M.IsFunction "core::slice::index::get_noubcheck" get_noubcheck.
    
    (*
    const unsafe fn get_mut_noubcheck<T>(ptr: *mut [T], index: usize) -> *mut T {
        let ptr = ptr as *mut T;
        // SAFETY: The caller already checked these preconditions
        unsafe { crate::intrinsics::offset(ptr, index) }
    }
    *)
    Definition get_mut_noubcheck (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ ptr; index ] =>
        ltac:(M.monadic
          (let ptr := M.alloc (| ptr |) in
          let index := M.alloc (| index |) in
          M.read (|
            let~ ptr := M.alloc (| M.rust_cast (M.read (| ptr |)) |) in
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::offset",
                  [ Ty.apply (Ty.path "*mut") [] [ T ]; Ty.path "usize" ]
                |),
                [ M.read (| ptr |); M.read (| index |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_get_mut_noubcheck :
      M.IsFunction "core::slice::index::get_mut_noubcheck" get_mut_noubcheck.
    
    (*
    const unsafe fn get_offset_len_noubcheck<T>(
        ptr: *const [T],
        offset: usize,
        len: usize,
    ) -> *const [T] {
        // SAFETY: The caller already checked these preconditions
        let ptr = unsafe { get_noubcheck(ptr, offset) };
        crate::intrinsics::aggregate_raw_ptr(ptr, len)
    }
    *)
    Definition get_offset_len_noubcheck (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ ptr; offset; len ] =>
        ltac:(M.monadic
          (let ptr := M.alloc (| ptr |) in
          let offset := M.alloc (| offset |) in
          let len := M.alloc (| len |) in
          M.read (|
            let~ ptr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::slice::index::get_noubcheck", [ T ] |),
                  [ M.read (| ptr |); M.read (| offset |) ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::aggregate_raw_ptr",
                  [
                    Ty.apply (Ty.path "*const") [] [ Ty.apply (Ty.path "slice") [] [ T ] ];
                    Ty.apply (Ty.path "*const") [] [ T ];
                    Ty.path "usize"
                  ]
                |),
                [ M.read (| ptr |); M.read (| len |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_get_offset_len_noubcheck :
      M.IsFunction "core::slice::index::get_offset_len_noubcheck" get_offset_len_noubcheck.
    
    (*
    const unsafe fn get_offset_len_mut_noubcheck<T>(
        ptr: *mut [T],
        offset: usize,
        len: usize,
    ) -> *mut [T] {
        // SAFETY: The caller already checked these preconditions
        let ptr = unsafe { get_mut_noubcheck(ptr, offset) };
        crate::intrinsics::aggregate_raw_ptr(ptr, len)
    }
    *)
    Definition get_offset_len_mut_noubcheck
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [ T ], [ ptr; offset; len ] =>
        ltac:(M.monadic
          (let ptr := M.alloc (| ptr |) in
          let offset := M.alloc (| offset |) in
          let len := M.alloc (| len |) in
          M.read (|
            let~ ptr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::slice::index::get_mut_noubcheck", [ T ] |),
                  [ M.read (| ptr |); M.read (| offset |) ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::aggregate_raw_ptr",
                  [
                    Ty.apply (Ty.path "*mut") [] [ Ty.apply (Ty.path "slice") [] [ T ] ];
                    Ty.apply (Ty.path "*mut") [] [ T ];
                    Ty.path "usize"
                  ]
                |),
                [ M.read (| ptr |); M.read (| len |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_get_offset_len_mut_noubcheck :
      M.IsFunction "core::slice::index::get_offset_len_mut_noubcheck" get_offset_len_mut_noubcheck.
    
    Module private_slice_index.
      (* Trait *)
      (* Empty module 'Sealed' *)
      
      Module Impl_core_slice_index_private_slice_index_Sealed_for_usize.
        Definition Self : Ty.t := Ty.path "usize".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::slice::index::private_slice_index::Sealed"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_slice_index_private_slice_index_Sealed_for_usize.
      
      Module Impl_core_slice_index_private_slice_index_Sealed_for_core_ops_range_Range_usize.
        Definition Self : Ty.t :=
          Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ].
        
        Axiom Implements :
          M.IsTraitInstance
            "core::slice::index::private_slice_index::Sealed"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_slice_index_private_slice_index_Sealed_for_core_ops_range_Range_usize.
      
      Module Impl_core_slice_index_private_slice_index_Sealed_for_core_ops_range_RangeTo_usize.
        Definition Self : Ty.t :=
          Ty.apply (Ty.path "core::ops::range::RangeTo") [] [ Ty.path "usize" ].
        
        Axiom Implements :
          M.IsTraitInstance
            "core::slice::index::private_slice_index::Sealed"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_slice_index_private_slice_index_Sealed_for_core_ops_range_RangeTo_usize.
      
      Module Impl_core_slice_index_private_slice_index_Sealed_for_core_ops_range_RangeFrom_usize.
        Definition Self : Ty.t :=
          Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ Ty.path "usize" ].
        
        Axiom Implements :
          M.IsTraitInstance
            "core::slice::index::private_slice_index::Sealed"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_slice_index_private_slice_index_Sealed_for_core_ops_range_RangeFrom_usize.
      
      Module Impl_core_slice_index_private_slice_index_Sealed_for_core_ops_range_RangeFull.
        Definition Self : Ty.t := Ty.path "core::ops::range::RangeFull".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::slice::index::private_slice_index::Sealed"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_slice_index_private_slice_index_Sealed_for_core_ops_range_RangeFull.
      
      Module Impl_core_slice_index_private_slice_index_Sealed_for_core_ops_range_RangeInclusive_usize.
        Definition Self : Ty.t :=
          Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ].
        
        Axiom Implements :
          M.IsTraitInstance
            "core::slice::index::private_slice_index::Sealed"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_slice_index_private_slice_index_Sealed_for_core_ops_range_RangeInclusive_usize.
      
      Module Impl_core_slice_index_private_slice_index_Sealed_for_core_ops_range_RangeToInclusive_usize.
        Definition Self : Ty.t :=
          Ty.apply (Ty.path "core::ops::range::RangeToInclusive") [] [ Ty.path "usize" ].
        
        Axiom Implements :
          M.IsTraitInstance
            "core::slice::index::private_slice_index::Sealed"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_slice_index_private_slice_index_Sealed_for_core_ops_range_RangeToInclusive_usize.
      
      Module Impl_core_slice_index_private_slice_index_Sealed_for_Tuple_core_ops_range_Bound_usize_core_ops_range_Bound_usize_.
        Definition Self : Ty.t :=
          Ty.tuple
            [
              Ty.apply (Ty.path "core::ops::range::Bound") [] [ Ty.path "usize" ];
              Ty.apply (Ty.path "core::ops::range::Bound") [] [ Ty.path "usize" ]
            ].
        
        Axiom Implements :
          M.IsTraitInstance
            "core::slice::index::private_slice_index::Sealed"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_slice_index_private_slice_index_Sealed_for_Tuple_core_ops_range_Bound_usize_core_ops_range_Bound_usize_.
      
      Module Impl_core_slice_index_private_slice_index_Sealed_for_core_range_Range_usize.
        Definition Self : Ty.t := Ty.apply (Ty.path "core::range::Range") [] [ Ty.path "usize" ].
        
        Axiom Implements :
          M.IsTraitInstance
            "core::slice::index::private_slice_index::Sealed"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_slice_index_private_slice_index_Sealed_for_core_range_Range_usize.
      
      Module Impl_core_slice_index_private_slice_index_Sealed_for_core_range_RangeInclusive_usize.
        Definition Self : Ty.t :=
          Ty.apply (Ty.path "core::range::RangeInclusive") [] [ Ty.path "usize" ].
        
        Axiom Implements :
          M.IsTraitInstance
            "core::slice::index::private_slice_index::Sealed"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_slice_index_private_slice_index_Sealed_for_core_range_RangeInclusive_usize.
      
      Module Impl_core_slice_index_private_slice_index_Sealed_for_core_range_RangeFrom_usize.
        Definition Self : Ty.t :=
          Ty.apply (Ty.path "core::range::RangeFrom") [] [ Ty.path "usize" ].
        
        Axiom Implements :
          M.IsTraitInstance
            "core::slice::index::private_slice_index::Sealed"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_slice_index_private_slice_index_Sealed_for_core_range_RangeFrom_usize.
      
      Module Impl_core_slice_index_private_slice_index_Sealed_for_core_ops_index_range_IndexRange.
        Definition Self : Ty.t := Ty.path "core::ops::index_range::IndexRange".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::slice::index::private_slice_index::Sealed"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_slice_index_private_slice_index_Sealed_for_core_ops_index_range_IndexRange.
    End private_slice_index.
    
    (* Trait *)
    (* Empty module 'SliceIndex' *)
    
    Module Impl_core_slice_index_SliceIndex_slice_T_for_usize.
      Definition Self (T : Ty.t) : Ty.t := Ty.path "usize".
      
      (*     type Output = T; *)
      Definition _Output (T : Ty.t) : Ty.t := T.
      
      (*
          fn get(self, slice: &[T]) -> Option<&T> {
              // SAFETY: `self` is checked to be in bounds.
              if self < slice.len() { unsafe { Some(&*get_noubcheck(slice, self)) } } else { None }
          }
      *)
      Definition get (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.lt (|
                              M.read (| self |),
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ T ],
                                  "len",
                                  []
                                |),
                                [ M.read (| slice |) ]
                              |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_function (| "core::slice::index::get_noubcheck", [ T ] |),
                              [ M.read (| slice |); M.read (| self |) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn get_mut(self, slice: &mut [T]) -> Option<&mut T> {
              if self < slice.len() {
                  // SAFETY: `self` is checked to be in bounds.
                  unsafe { Some(&mut *get_mut_noubcheck(slice, self)) }
              } else {
                  None
              }
          }
      *)
      Definition get_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.lt (|
                              M.read (| self |),
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ T ],
                                  "len",
                                  []
                                |),
                                [ M.read (| slice |) ]
                              |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_function (| "core::slice::index::get_mut_noubcheck", [ T ] |),
                              [ M.read (| slice |); M.read (| self |) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked(self, slice: *const [T]) -> *const T {
              assert_unsafe_precondition!(
                  check_language_ub,
                  "slice::get_unchecked requires that the index is within the slice",
                  (this: usize = self, len: usize = slice.len()) => this < len
              );
              // SAFETY: the caller guarantees that `slice` is not dangling, so it
              // cannot be longer than `isize::MAX`. They also guarantee that
              // `self` is in bounds of `slice` so `self` cannot overflow an `isize`,
              // so the call to `add` is safe.
              unsafe {
                  // Use intrinsics::assume instead of hint::assert_unchecked so that we don't check the
                  // precondition of this function twice.
                  crate::intrinsics::assume(self < slice.len());
                  get_noubcheck(slice, self)
              }
          }
      *)
      Definition get_unchecked
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_function (| "core::ub_checks::check_language_ub", [] |),
                                []
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Self,
                                "precondition_check.get_unchecked",
                                []
                              |),
                              [
                                M.read (| self |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "*const")
                                      []
                                      [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| slice |) ]
                                |)
                              ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::intrinsics::assume", [] |),
                    [
                      BinOp.lt (|
                        M.read (| self |),
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "*const") [] [ Ty.apply (Ty.path "slice") [] [ T ] ],
                            "len",
                            []
                          |),
                          [ M.read (| slice |) ]
                        |)
                      |)
                    ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::slice::index::get_noubcheck", [ T ] |),
                  [ M.read (| slice |); M.read (| self |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked_mut(self, slice: *mut [T]) -> *mut T {
              assert_unsafe_precondition!(
                  check_library_ub,
                  "slice::get_unchecked_mut requires that the index is within the slice",
                  (this: usize = self, len: usize = slice.len()) => this < len
              );
              // SAFETY: see comments for `get_unchecked` above.
              unsafe { get_mut_noubcheck(slice, self) }
          }
      *)
      Definition get_unchecked_mut
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_function (| "core::intrinsics::ub_checks", [] |),
                                []
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Self,
                                "precondition_check.get_unchecked_mut",
                                []
                              |),
                              [
                                M.read (| self |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "*mut")
                                      []
                                      [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| slice |) ]
                                |)
                              ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::slice::index::get_mut_noubcheck", [ T ] |),
                  [ M.read (| slice |); M.read (| self |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index(self, slice: &[T]) -> &T {
              // N.B., use intrinsic indexing
              &( *slice)[self]
          }
      *)
      Definition index (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.SubPointer.get_array_field (| M.read (| slice |), self |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index_mut(self, slice: &mut [T]) -> &mut T {
              // N.B., use intrinsic indexing
              &mut ( *slice)[self]
          }
      *)
      Definition index_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.SubPointer.get_array_field (| M.read (| slice |), self |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::slice::index::SliceIndex"
          (Self T)
          (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "slice") [] [ T ] ]
          (* Instance *)
          [
            ("Output", InstanceField.Ty (_Output T));
            ("get", InstanceField.Method (get T));
            ("get_mut", InstanceField.Method (get_mut T));
            ("get_unchecked", InstanceField.Method (get_unchecked T));
            ("get_unchecked_mut", InstanceField.Method (get_unchecked_mut T));
            ("index", InstanceField.Method (index T));
            ("index_mut", InstanceField.Method (index_mut T))
          ].
    End Impl_core_slice_index_SliceIndex_slice_T_for_usize.
    
    Module Impl_core_slice_index_SliceIndex_slice_T_for_core_ops_index_range_IndexRange.
      Definition Self (T : Ty.t) : Ty.t := Ty.path "core::ops::index_range::IndexRange".
      
      (*     type Output = [T]; *)
      Definition _Output (T : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ T ].
      
      (*
          fn get(self, slice: &[T]) -> Option<&[T]> {
              if self.end() <= slice.len() {
                  // SAFETY: `self` is checked to be valid and in bounds above.
                  unsafe { Some(&*get_offset_len_noubcheck(slice, self.start(), self.len())) }
              } else {
                  None
              }
          }
      *)
      Definition get (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.le (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::ops::index_range::IndexRange",
                                  "end",
                                  []
                                |),
                                [ self ]
                              |),
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ T ],
                                  "len",
                                  []
                                |),
                                [ M.read (| slice |) ]
                              |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_function (|
                                "core::slice::index::get_offset_len_noubcheck",
                                [ T ]
                              |),
                              [
                                M.read (| slice |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "core::ops::index_range::IndexRange",
                                    "start",
                                    []
                                  |),
                                  [ self ]
                                |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "core::ops::index_range::IndexRange",
                                    "len",
                                    []
                                  |),
                                  [ self ]
                                |)
                              ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn get_mut(self, slice: &mut [T]) -> Option<&mut [T]> {
              if self.end() <= slice.len() {
                  // SAFETY: `self` is checked to be valid and in bounds above.
                  unsafe { Some(&mut *get_offset_len_mut_noubcheck(slice, self.start(), self.len())) }
              } else {
                  None
              }
          }
      *)
      Definition get_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.le (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::ops::index_range::IndexRange",
                                  "end",
                                  []
                                |),
                                [ self ]
                              |),
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ T ],
                                  "len",
                                  []
                                |),
                                [ M.read (| slice |) ]
                              |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_function (|
                                "core::slice::index::get_offset_len_mut_noubcheck",
                                [ T ]
                              |),
                              [
                                M.read (| slice |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "core::ops::index_range::IndexRange",
                                    "start",
                                    []
                                  |),
                                  [ self ]
                                |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "core::ops::index_range::IndexRange",
                                    "len",
                                    []
                                  |),
                                  [ self ]
                                |)
                              ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked(self, slice: *const [T]) -> *const [T] {
              assert_unsafe_precondition!(
                  check_library_ub,
                  "slice::get_unchecked requires that the index is within the slice",
                  (end: usize = self.end(), len: usize = slice.len()) => end <= len
              );
              // SAFETY: the caller guarantees that `slice` is not dangling, so it
              // cannot be longer than `isize::MAX`. They also guarantee that
              // `self` is in bounds of `slice` so `self` cannot overflow an `isize`,
              // so the call to `add` is safe.
              unsafe { get_offset_len_noubcheck(slice, self.start(), self.len()) }
          }
      *)
      Definition get_unchecked
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_function (| "core::intrinsics::ub_checks", [] |),
                                []
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Self,
                                "precondition_check.get_unchecked",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "core::ops::index_range::IndexRange",
                                    "end",
                                    []
                                  |),
                                  [ self ]
                                |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "*const")
                                      []
                                      [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| slice |) ]
                                |)
                              ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::slice::index::get_offset_len_noubcheck", [ T ] |),
                  [
                    M.read (| slice |);
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::ops::index_range::IndexRange",
                        "start",
                        []
                      |),
                      [ self ]
                    |);
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::ops::index_range::IndexRange",
                        "len",
                        []
                      |),
                      [ self ]
                    |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked_mut(self, slice: *mut [T]) -> *mut [T] {
              assert_unsafe_precondition!(
                  check_library_ub,
                  "slice::get_unchecked_mut requires that the index is within the slice",
                  (end: usize = self.end(), len: usize = slice.len()) => end <= len
              );
      
              // SAFETY: see comments for `get_unchecked` above.
              unsafe { get_offset_len_mut_noubcheck(slice, self.start(), self.len()) }
          }
      *)
      Definition get_unchecked_mut
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_function (| "core::intrinsics::ub_checks", [] |),
                                []
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Self,
                                "precondition_check.get_unchecked_mut",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "core::ops::index_range::IndexRange",
                                    "end",
                                    []
                                  |),
                                  [ self ]
                                |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "*mut")
                                      []
                                      [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| slice |) ]
                                |)
                              ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::slice::index::get_offset_len_mut_noubcheck", [ T ] |),
                  [
                    M.read (| slice |);
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::ops::index_range::IndexRange",
                        "start",
                        []
                      |),
                      [ self ]
                    |);
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::ops::index_range::IndexRange",
                        "len",
                        []
                      |),
                      [ self ]
                    |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index(self, slice: &[T]) -> &[T] {
              if self.end() <= slice.len() {
                  // SAFETY: `self` is checked to be valid and in bounds above.
                  unsafe { &*get_offset_len_noubcheck(slice, self.start(), self.len()) }
              } else {
                  slice_end_index_len_fail(self.end(), slice.len())
              }
          }
      *)
      Definition index (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.le (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::ops::index_range::IndexRange",
                                  "end",
                                  []
                                |),
                                [ self ]
                              |),
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ T ],
                                  "len",
                                  []
                                |),
                                [ M.read (| slice |) ]
                              |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (|
                            "core::slice::index::get_offset_len_noubcheck",
                            [ T ]
                          |),
                          [
                            M.read (| slice |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::ops::index_range::IndexRange",
                                "start",
                                []
                              |),
                              [ self ]
                            |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::ops::index_range::IndexRange",
                                "len",
                                []
                              |),
                              [ self ]
                            |)
                          ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.never_to_any (|
                          M.call_closure (|
                            M.get_function (| "core::slice::index::slice_end_index_len_fail", [] |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::ops::index_range::IndexRange",
                                  "end",
                                  []
                                |),
                                [ self ]
                              |);
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ T ],
                                  "len",
                                  []
                                |),
                                [ M.read (| slice |) ]
                              |)
                            ]
                          |)
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index_mut(self, slice: &mut [T]) -> &mut [T] {
              if self.end() <= slice.len() {
                  // SAFETY: `self` is checked to be valid and in bounds above.
                  unsafe { &mut *get_offset_len_mut_noubcheck(slice, self.start(), self.len()) }
              } else {
                  slice_end_index_len_fail(self.end(), slice.len())
              }
          }
      *)
      Definition index_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.le (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::ops::index_range::IndexRange",
                                  "end",
                                  []
                                |),
                                [ self ]
                              |),
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ T ],
                                  "len",
                                  []
                                |),
                                [ M.read (| slice |) ]
                              |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (|
                            "core::slice::index::get_offset_len_mut_noubcheck",
                            [ T ]
                          |),
                          [
                            M.read (| slice |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::ops::index_range::IndexRange",
                                "start",
                                []
                              |),
                              [ self ]
                            |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::ops::index_range::IndexRange",
                                "len",
                                []
                              |),
                              [ self ]
                            |)
                          ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.never_to_any (|
                          M.call_closure (|
                            M.get_function (| "core::slice::index::slice_end_index_len_fail", [] |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::ops::index_range::IndexRange",
                                  "end",
                                  []
                                |),
                                [ self ]
                              |);
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ T ],
                                  "len",
                                  []
                                |),
                                [ M.read (| slice |) ]
                              |)
                            ]
                          |)
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::slice::index::SliceIndex"
          (Self T)
          (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "slice") [] [ T ] ]
          (* Instance *)
          [
            ("Output", InstanceField.Ty (_Output T));
            ("get", InstanceField.Method (get T));
            ("get_mut", InstanceField.Method (get_mut T));
            ("get_unchecked", InstanceField.Method (get_unchecked T));
            ("get_unchecked_mut", InstanceField.Method (get_unchecked_mut T));
            ("index", InstanceField.Method (index T));
            ("index_mut", InstanceField.Method (index_mut T))
          ].
    End Impl_core_slice_index_SliceIndex_slice_T_for_core_ops_index_range_IndexRange.
    
    Module Impl_core_slice_index_SliceIndex_slice_T_for_core_ops_range_Range_usize.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ].
      
      (*     type Output = [T]; *)
      Definition _Output (T : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ T ].
      
      (*
          fn get(self, slice: &[T]) -> Option<&[T]> {
              // Using checked_sub is a safe way to get `SubUnchecked` in MIR
              if let Some(new_len) = usize::checked_sub(self.end, self.start)
                  && self.end <= slice.len()
              {
                  // SAFETY: `self` is checked to be valid and in bounds above.
                  unsafe { Some(&*get_offset_len_noubcheck(slice, self.start, new_len)) }
              } else {
                  None
              }
          }
      *)
      Definition get (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (| Ty.path "usize", "checked_sub", [] |),
                            [
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  self,
                                  "core::ops::range::Range",
                                  "end"
                                |)
                              |);
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  self,
                                  "core::ops::range::Range",
                                  "start"
                                |)
                              |)
                            ]
                          |)
                        |) in
                      let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let new_len := M.copy (| γ0_0 |) in
                      let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.le (|
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  self,
                                  "core::ops::range::Range",
                                  "end"
                                |)
                              |),
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ T ],
                                  "len",
                                  []
                                |),
                                [ M.read (| slice |) ]
                              |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_function (|
                                "core::slice::index::get_offset_len_noubcheck",
                                [ T ]
                              |),
                              [
                                M.read (| slice |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::ops::range::Range",
                                    "start"
                                  |)
                                |);
                                M.read (| new_len |)
                              ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn get_mut(self, slice: &mut [T]) -> Option<&mut [T]> {
              if let Some(new_len) = usize::checked_sub(self.end, self.start)
                  && self.end <= slice.len()
              {
                  // SAFETY: `self` is checked to be valid and in bounds above.
                  unsafe { Some(&mut *get_offset_len_mut_noubcheck(slice, self.start, new_len)) }
              } else {
                  None
              }
          }
      *)
      Definition get_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (| Ty.path "usize", "checked_sub", [] |),
                            [
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  self,
                                  "core::ops::range::Range",
                                  "end"
                                |)
                              |);
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  self,
                                  "core::ops::range::Range",
                                  "start"
                                |)
                              |)
                            ]
                          |)
                        |) in
                      let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let new_len := M.copy (| γ0_0 |) in
                      let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.le (|
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  self,
                                  "core::ops::range::Range",
                                  "end"
                                |)
                              |),
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ T ],
                                  "len",
                                  []
                                |),
                                [ M.read (| slice |) ]
                              |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_function (|
                                "core::slice::index::get_offset_len_mut_noubcheck",
                                [ T ]
                              |),
                              [
                                M.read (| slice |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::ops::range::Range",
                                    "start"
                                  |)
                                |);
                                M.read (| new_len |)
                              ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked(self, slice: *const [T]) -> *const [T] {
              assert_unsafe_precondition!(
                  check_library_ub,
                  "slice::get_unchecked requires that the range is within the slice",
                  (
                      start: usize = self.start,
                      end: usize = self.end,
                      len: usize = slice.len()
                  ) => end >= start && end <= len
              );
      
              // SAFETY: the caller guarantees that `slice` is not dangling, so it
              // cannot be longer than `isize::MAX`. They also guarantee that
              // `self` is in bounds of `slice` so `self` cannot overflow an `isize`,
              // so the call to `add` is safe and the length calculation cannot overflow.
              unsafe {
                  // Using the intrinsic avoids a superfluous UB check,
                  // since the one on this method already checked `end >= start`.
                  let new_len = crate::intrinsics::unchecked_sub(self.end, self.start);
                  get_offset_len_noubcheck(slice, self.start, new_len)
              }
          }
      *)
      Definition get_unchecked
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_function (| "core::intrinsics::ub_checks", [] |),
                                []
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Self,
                                "precondition_check.get_unchecked",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::ops::range::Range",
                                    "start"
                                  |)
                                |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::ops::range::Range",
                                    "end"
                                  |)
                                |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "*const")
                                      []
                                      [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| slice |) ]
                                |)
                              ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ new_len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::intrinsics::unchecked_sub", [ Ty.path "usize" ] |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::Range",
                          "end"
                        |)
                      |);
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::Range",
                          "start"
                        |)
                      |)
                    ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::slice::index::get_offset_len_noubcheck", [ T ] |),
                  [
                    M.read (| slice |);
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        self,
                        "core::ops::range::Range",
                        "start"
                      |)
                    |);
                    M.read (| new_len |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked_mut(self, slice: *mut [T]) -> *mut [T] {
              assert_unsafe_precondition!(
                  check_library_ub,
                  "slice::get_unchecked_mut requires that the range is within the slice",
                  (
                      start: usize = self.start,
                      end: usize = self.end,
                      len: usize = slice.len()
                  ) => end >= start && end <= len
              );
              // SAFETY: see comments for `get_unchecked` above.
              unsafe {
                  let new_len = crate::intrinsics::unchecked_sub(self.end, self.start);
                  get_offset_len_mut_noubcheck(slice, self.start, new_len)
              }
          }
      *)
      Definition get_unchecked_mut
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_function (| "core::intrinsics::ub_checks", [] |),
                                []
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Self,
                                "precondition_check.get_unchecked_mut",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::ops::range::Range",
                                    "start"
                                  |)
                                |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::ops::range::Range",
                                    "end"
                                  |)
                                |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "*mut")
                                      []
                                      [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| slice |) ]
                                |)
                              ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ new_len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::intrinsics::unchecked_sub", [ Ty.path "usize" ] |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::Range",
                          "end"
                        |)
                      |);
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::Range",
                          "start"
                        |)
                      |)
                    ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::slice::index::get_offset_len_mut_noubcheck", [ T ] |),
                  [
                    M.read (| slice |);
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        self,
                        "core::ops::range::Range",
                        "start"
                      |)
                    |);
                    M.read (| new_len |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index(self, slice: &[T]) -> &[T] {
              // Using checked_sub is a safe way to get `SubUnchecked` in MIR
              let Some(new_len) = usize::checked_sub(self.end, self.start) else {
                  slice_index_order_fail(self.start, self.end)
              };
              if self.end > slice.len() {
                  slice_end_index_len_fail(self.end, slice.len());
              }
              // SAFETY: `self` is checked to be valid and in bounds above.
              unsafe { &*get_offset_len_noubcheck(slice, self.start, new_len) }
          }
      *)
      Definition index (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "usize", "checked_sub", [] |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::Range",
                          "end"
                        |)
                      |);
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::Range",
                          "start"
                        |)
                      |)
                    ]
                  |)
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let new_len := M.copy (| γ0_0 |) in
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      BinOp.gt (|
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            self,
                                            "core::ops::range::Range",
                                            "end"
                                          |)
                                        |),
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply (Ty.path "slice") [] [ T ],
                                            "len",
                                            []
                                          |),
                                          [ M.read (| slice |) ]
                                        |)
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.call_closure (|
                                      M.get_function (|
                                        "core::slice::index::slice_end_index_len_fail",
                                        []
                                      |),
                                      [
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            self,
                                            "core::ops::range::Range",
                                            "end"
                                          |)
                                        |);
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply (Ty.path "slice") [] [ T ],
                                            "len",
                                            []
                                          |),
                                          [ M.read (| slice |) ]
                                        |)
                                      ]
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (|
                            "core::slice::index::get_offset_len_noubcheck",
                            [ T ]
                          |),
                          [
                            M.read (| slice |);
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                self,
                                "core::ops::range::Range",
                                "start"
                              |)
                            |);
                            M.read (| new_len |)
                          ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index_mut(self, slice: &mut [T]) -> &mut [T] {
              let Some(new_len) = usize::checked_sub(self.end, self.start) else {
                  slice_index_order_fail(self.start, self.end)
              };
              if self.end > slice.len() {
                  slice_end_index_len_fail(self.end, slice.len());
              }
              // SAFETY: `self` is checked to be valid and in bounds above.
              unsafe { &mut *get_offset_len_mut_noubcheck(slice, self.start, new_len) }
          }
      *)
      Definition index_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "usize", "checked_sub", [] |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::Range",
                          "end"
                        |)
                      |);
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::Range",
                          "start"
                        |)
                      |)
                    ]
                  |)
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let new_len := M.copy (| γ0_0 |) in
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      BinOp.gt (|
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            self,
                                            "core::ops::range::Range",
                                            "end"
                                          |)
                                        |),
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply (Ty.path "slice") [] [ T ],
                                            "len",
                                            []
                                          |),
                                          [ M.read (| slice |) ]
                                        |)
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.call_closure (|
                                      M.get_function (|
                                        "core::slice::index::slice_end_index_len_fail",
                                        []
                                      |),
                                      [
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            self,
                                            "core::ops::range::Range",
                                            "end"
                                          |)
                                        |);
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply (Ty.path "slice") [] [ T ],
                                            "len",
                                            []
                                          |),
                                          [ M.read (| slice |) ]
                                        |)
                                      ]
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (|
                            "core::slice::index::get_offset_len_mut_noubcheck",
                            [ T ]
                          |),
                          [
                            M.read (| slice |);
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                self,
                                "core::ops::range::Range",
                                "start"
                              |)
                            |);
                            M.read (| new_len |)
                          ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::slice::index::SliceIndex"
          (Self T)
          (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "slice") [] [ T ] ]
          (* Instance *)
          [
            ("Output", InstanceField.Ty (_Output T));
            ("get", InstanceField.Method (get T));
            ("get_mut", InstanceField.Method (get_mut T));
            ("get_unchecked", InstanceField.Method (get_unchecked T));
            ("get_unchecked_mut", InstanceField.Method (get_unchecked_mut T));
            ("index", InstanceField.Method (index T));
            ("index_mut", InstanceField.Method (index_mut T))
          ].
    End Impl_core_slice_index_SliceIndex_slice_T_for_core_ops_range_Range_usize.
    
    Module Impl_core_slice_index_SliceIndex_slice_T_for_core_range_Range_usize.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::range::Range") [] [ Ty.path "usize" ].
      
      (*     type Output = [T]; *)
      Definition _Output (T : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ T ].
      
      (*
          fn get(self, slice: &[T]) -> Option<&[T]> {
              ops::Range::from(self).get(slice)
          }
      *)
      Definition get (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::From",
                    Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                    [ Ty.apply (Ty.path "core::range::Range") [] [ Ty.path "usize" ] ],
                    "from",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn get_mut(self, slice: &mut [T]) -> Option<&mut [T]> {
              ops::Range::from(self).get_mut(slice)
          }
      *)
      Definition get_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get_mut",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::From",
                    Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                    [ Ty.apply (Ty.path "core::range::Range") [] [ Ty.path "usize" ] ],
                    "from",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked(self, slice: *const [T]) -> *const [T] {
              // SAFETY: the caller has to uphold the safety contract for `get_unchecked`.
              unsafe { ops::Range::from(self).get_unchecked(slice) }
          }
      *)
      Definition get_unchecked
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get_unchecked",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::From",
                    Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                    [ Ty.apply (Ty.path "core::range::Range") [] [ Ty.path "usize" ] ],
                    "from",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked_mut(self, slice: *mut [T]) -> *mut [T] {
              // SAFETY: the caller has to uphold the safety contract for `get_unchecked_mut`.
              unsafe { ops::Range::from(self).get_unchecked_mut(slice) }
          }
      *)
      Definition get_unchecked_mut
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get_unchecked_mut",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::From",
                    Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                    [ Ty.apply (Ty.path "core::range::Range") [] [ Ty.path "usize" ] ],
                    "from",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index(self, slice: &[T]) -> &[T] {
              ops::Range::from(self).index(slice)
          }
      *)
      Definition index (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "index",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::From",
                    Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                    [ Ty.apply (Ty.path "core::range::Range") [] [ Ty.path "usize" ] ],
                    "from",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index_mut(self, slice: &mut [T]) -> &mut [T] {
              ops::Range::from(self).index_mut(slice)
          }
      *)
      Definition index_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "index_mut",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::From",
                    Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                    [ Ty.apply (Ty.path "core::range::Range") [] [ Ty.path "usize" ] ],
                    "from",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::slice::index::SliceIndex"
          (Self T)
          (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "slice") [] [ T ] ]
          (* Instance *)
          [
            ("Output", InstanceField.Ty (_Output T));
            ("get", InstanceField.Method (get T));
            ("get_mut", InstanceField.Method (get_mut T));
            ("get_unchecked", InstanceField.Method (get_unchecked T));
            ("get_unchecked_mut", InstanceField.Method (get_unchecked_mut T));
            ("index", InstanceField.Method (index T));
            ("index_mut", InstanceField.Method (index_mut T))
          ].
    End Impl_core_slice_index_SliceIndex_slice_T_for_core_range_Range_usize.
    
    Module Impl_core_slice_index_SliceIndex_slice_T_for_core_ops_range_RangeTo_usize.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::range::RangeTo") [] [ Ty.path "usize" ].
      
      (*     type Output = [T]; *)
      Definition _Output (T : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ T ].
      
      (*
          fn get(self, slice: &[T]) -> Option<&[T]> {
              (0..self.end).get(slice)
          }
      *)
      Definition get (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get",
                []
              |),
              [
                Value.StructRecord
                  "core::ops::range::Range"
                  [
                    ("start", Value.Integer IntegerKind.Usize 0);
                    ("end_",
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::RangeTo",
                          "end"
                        |)
                      |))
                  ];
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn get_mut(self, slice: &mut [T]) -> Option<&mut [T]> {
              (0..self.end).get_mut(slice)
          }
      *)
      Definition get_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get_mut",
                []
              |),
              [
                Value.StructRecord
                  "core::ops::range::Range"
                  [
                    ("start", Value.Integer IntegerKind.Usize 0);
                    ("end_",
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::RangeTo",
                          "end"
                        |)
                      |))
                  ];
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked(self, slice: *const [T]) -> *const [T] {
              // SAFETY: the caller has to uphold the safety contract for `get_unchecked`.
              unsafe { (0..self.end).get_unchecked(slice) }
          }
      *)
      Definition get_unchecked
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get_unchecked",
                []
              |),
              [
                Value.StructRecord
                  "core::ops::range::Range"
                  [
                    ("start", Value.Integer IntegerKind.Usize 0);
                    ("end_",
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::RangeTo",
                          "end"
                        |)
                      |))
                  ];
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked_mut(self, slice: *mut [T]) -> *mut [T] {
              // SAFETY: the caller has to uphold the safety contract for `get_unchecked_mut`.
              unsafe { (0..self.end).get_unchecked_mut(slice) }
          }
      *)
      Definition get_unchecked_mut
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get_unchecked_mut",
                []
              |),
              [
                Value.StructRecord
                  "core::ops::range::Range"
                  [
                    ("start", Value.Integer IntegerKind.Usize 0);
                    ("end_",
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::RangeTo",
                          "end"
                        |)
                      |))
                  ];
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index(self, slice: &[T]) -> &[T] {
              (0..self.end).index(slice)
          }
      *)
      Definition index (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "index",
                []
              |),
              [
                Value.StructRecord
                  "core::ops::range::Range"
                  [
                    ("start", Value.Integer IntegerKind.Usize 0);
                    ("end_",
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::RangeTo",
                          "end"
                        |)
                      |))
                  ];
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index_mut(self, slice: &mut [T]) -> &mut [T] {
              (0..self.end).index_mut(slice)
          }
      *)
      Definition index_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "index_mut",
                []
              |),
              [
                Value.StructRecord
                  "core::ops::range::Range"
                  [
                    ("start", Value.Integer IntegerKind.Usize 0);
                    ("end_",
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::RangeTo",
                          "end"
                        |)
                      |))
                  ];
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::slice::index::SliceIndex"
          (Self T)
          (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "slice") [] [ T ] ]
          (* Instance *)
          [
            ("Output", InstanceField.Ty (_Output T));
            ("get", InstanceField.Method (get T));
            ("get_mut", InstanceField.Method (get_mut T));
            ("get_unchecked", InstanceField.Method (get_unchecked T));
            ("get_unchecked_mut", InstanceField.Method (get_unchecked_mut T));
            ("index", InstanceField.Method (index T));
            ("index_mut", InstanceField.Method (index_mut T))
          ].
    End Impl_core_slice_index_SliceIndex_slice_T_for_core_ops_range_RangeTo_usize.
    
    Module Impl_core_slice_index_SliceIndex_slice_T_for_core_ops_range_RangeFrom_usize.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ Ty.path "usize" ].
      
      (*     type Output = [T]; *)
      Definition _Output (T : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ T ].
      
      (*
          fn get(self, slice: &[T]) -> Option<&[T]> {
              (self.start..slice.len()).get(slice)
          }
      *)
      Definition get (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get",
                []
              |),
              [
                Value.StructRecord
                  "core::ops::range::Range"
                  [
                    ("start",
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::RangeFrom",
                          "start"
                        |)
                      |));
                    ("end_",
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ T ],
                          "len",
                          []
                        |),
                        [ M.read (| slice |) ]
                      |))
                  ];
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn get_mut(self, slice: &mut [T]) -> Option<&mut [T]> {
              (self.start..slice.len()).get_mut(slice)
          }
      *)
      Definition get_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get_mut",
                []
              |),
              [
                Value.StructRecord
                  "core::ops::range::Range"
                  [
                    ("start",
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::RangeFrom",
                          "start"
                        |)
                      |));
                    ("end_",
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ T ],
                          "len",
                          []
                        |),
                        [ M.read (| slice |) ]
                      |))
                  ];
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked(self, slice: *const [T]) -> *const [T] {
              // SAFETY: the caller has to uphold the safety contract for `get_unchecked`.
              unsafe { (self.start..slice.len()).get_unchecked(slice) }
          }
      *)
      Definition get_unchecked
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get_unchecked",
                []
              |),
              [
                Value.StructRecord
                  "core::ops::range::Range"
                  [
                    ("start",
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::RangeFrom",
                          "start"
                        |)
                      |));
                    ("end_",
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "*const") [] [ Ty.apply (Ty.path "slice") [] [ T ] ],
                          "len",
                          []
                        |),
                        [ M.read (| slice |) ]
                      |))
                  ];
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked_mut(self, slice: *mut [T]) -> *mut [T] {
              // SAFETY: the caller has to uphold the safety contract for `get_unchecked_mut`.
              unsafe { (self.start..slice.len()).get_unchecked_mut(slice) }
          }
      *)
      Definition get_unchecked_mut
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get_unchecked_mut",
                []
              |),
              [
                Value.StructRecord
                  "core::ops::range::Range"
                  [
                    ("start",
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::RangeFrom",
                          "start"
                        |)
                      |));
                    ("end_",
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "*mut") [] [ Ty.apply (Ty.path "slice") [] [ T ] ],
                          "len",
                          []
                        |),
                        [ M.read (| slice |) ]
                      |))
                  ];
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index(self, slice: &[T]) -> &[T] {
              if self.start > slice.len() {
                  slice_start_index_len_fail(self.start, slice.len());
              }
              // SAFETY: `self` is checked to be valid and in bounds above.
              unsafe { &*self.get_unchecked(slice) }
          }
      *)
      Definition index (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.gt (|
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::ops::range::RangeFrom",
                                    "start"
                                  |)
                                |),
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "slice") [] [ T ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| slice |) ]
                                |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.call_closure (|
                              M.get_function (|
                                "core::slice::index::slice_start_index_len_fail",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::ops::range::RangeFrom",
                                    "start"
                                  |)
                                |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "slice") [] [ T ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| slice |) ]
                                |)
                              ]
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::slice::index::SliceIndex",
                    Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ Ty.path "usize" ],
                    [ Ty.apply (Ty.path "slice") [] [ T ] ],
                    "get_unchecked",
                    []
                  |),
                  [ M.read (| self |); M.read (| slice |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index_mut(self, slice: &mut [T]) -> &mut [T] {
              if self.start > slice.len() {
                  slice_start_index_len_fail(self.start, slice.len());
              }
              // SAFETY: `self` is checked to be valid and in bounds above.
              unsafe { &mut *self.get_unchecked_mut(slice) }
          }
      *)
      Definition index_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.gt (|
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::ops::range::RangeFrom",
                                    "start"
                                  |)
                                |),
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "slice") [] [ T ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| slice |) ]
                                |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.call_closure (|
                              M.get_function (|
                                "core::slice::index::slice_start_index_len_fail",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::ops::range::RangeFrom",
                                    "start"
                                  |)
                                |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "slice") [] [ T ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| slice |) ]
                                |)
                              ]
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::slice::index::SliceIndex",
                    Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ Ty.path "usize" ],
                    [ Ty.apply (Ty.path "slice") [] [ T ] ],
                    "get_unchecked_mut",
                    []
                  |),
                  [ M.read (| self |); M.read (| slice |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::slice::index::SliceIndex"
          (Self T)
          (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "slice") [] [ T ] ]
          (* Instance *)
          [
            ("Output", InstanceField.Ty (_Output T));
            ("get", InstanceField.Method (get T));
            ("get_mut", InstanceField.Method (get_mut T));
            ("get_unchecked", InstanceField.Method (get_unchecked T));
            ("get_unchecked_mut", InstanceField.Method (get_unchecked_mut T));
            ("index", InstanceField.Method (index T));
            ("index_mut", InstanceField.Method (index_mut T))
          ].
    End Impl_core_slice_index_SliceIndex_slice_T_for_core_ops_range_RangeFrom_usize.
    
    Module Impl_core_slice_index_SliceIndex_slice_T_for_core_range_RangeFrom_usize.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::range::RangeFrom") [] [ Ty.path "usize" ].
      
      (*     type Output = [T]; *)
      Definition _Output (T : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ T ].
      
      (*
          fn get(self, slice: &[T]) -> Option<&[T]> {
              ops::RangeFrom::from(self).get(slice)
          }
      *)
      Definition get (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::From",
                    Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ Ty.path "usize" ],
                    [ Ty.apply (Ty.path "core::range::RangeFrom") [] [ Ty.path "usize" ] ],
                    "from",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn get_mut(self, slice: &mut [T]) -> Option<&mut [T]> {
              ops::RangeFrom::from(self).get_mut(slice)
          }
      *)
      Definition get_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get_mut",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::From",
                    Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ Ty.path "usize" ],
                    [ Ty.apply (Ty.path "core::range::RangeFrom") [] [ Ty.path "usize" ] ],
                    "from",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked(self, slice: *const [T]) -> *const [T] {
              // SAFETY: the caller has to uphold the safety contract for `get_unchecked`.
              unsafe { ops::RangeFrom::from(self).get_unchecked(slice) }
          }
      *)
      Definition get_unchecked
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get_unchecked",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::From",
                    Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ Ty.path "usize" ],
                    [ Ty.apply (Ty.path "core::range::RangeFrom") [] [ Ty.path "usize" ] ],
                    "from",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked_mut(self, slice: *mut [T]) -> *mut [T] {
              // SAFETY: the caller has to uphold the safety contract for `get_unchecked_mut`.
              unsafe { ops::RangeFrom::from(self).get_unchecked_mut(slice) }
          }
      *)
      Definition get_unchecked_mut
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get_unchecked_mut",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::From",
                    Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ Ty.path "usize" ],
                    [ Ty.apply (Ty.path "core::range::RangeFrom") [] [ Ty.path "usize" ] ],
                    "from",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index(self, slice: &[T]) -> &[T] {
              ops::RangeFrom::from(self).index(slice)
          }
      *)
      Definition index (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "index",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::From",
                    Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ Ty.path "usize" ],
                    [ Ty.apply (Ty.path "core::range::RangeFrom") [] [ Ty.path "usize" ] ],
                    "from",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index_mut(self, slice: &mut [T]) -> &mut [T] {
              ops::RangeFrom::from(self).index_mut(slice)
          }
      *)
      Definition index_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "index_mut",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::From",
                    Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ Ty.path "usize" ],
                    [ Ty.apply (Ty.path "core::range::RangeFrom") [] [ Ty.path "usize" ] ],
                    "from",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::slice::index::SliceIndex"
          (Self T)
          (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "slice") [] [ T ] ]
          (* Instance *)
          [
            ("Output", InstanceField.Ty (_Output T));
            ("get", InstanceField.Method (get T));
            ("get_mut", InstanceField.Method (get_mut T));
            ("get_unchecked", InstanceField.Method (get_unchecked T));
            ("get_unchecked_mut", InstanceField.Method (get_unchecked_mut T));
            ("index", InstanceField.Method (index T));
            ("index_mut", InstanceField.Method (index_mut T))
          ].
    End Impl_core_slice_index_SliceIndex_slice_T_for_core_range_RangeFrom_usize.
    
    Module Impl_core_slice_index_SliceIndex_slice_T_for_core_ops_range_RangeFull.
      Definition Self (T : Ty.t) : Ty.t := Ty.path "core::ops::range::RangeFull".
      
      (*     type Output = [T]; *)
      Definition _Output (T : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ T ].
      
      (*
          fn get(self, slice: &[T]) -> Option<&[T]> {
              Some(slice)
          }
      *)
      Definition get (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            Value.StructTuple "core::option::Option::Some" [ M.read (| slice |) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn get_mut(self, slice: &mut [T]) -> Option<&mut [T]> {
              Some(slice)
          }
      *)
      Definition get_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            Value.StructTuple "core::option::Option::Some" [ M.read (| slice |) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked(self, slice: *const [T]) -> *const [T] {
              slice
          }
      *)
      Definition get_unchecked
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (| slice |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked_mut(self, slice: *mut [T]) -> *mut [T] {
              slice
          }
      *)
      Definition get_unchecked_mut
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (| slice |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index(self, slice: &[T]) -> &[T] {
              slice
          }
      *)
      Definition index (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (| slice |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index_mut(self, slice: &mut [T]) -> &mut [T] {
              slice
          }
      *)
      Definition index_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (| slice |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::slice::index::SliceIndex"
          (Self T)
          (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "slice") [] [ T ] ]
          (* Instance *)
          [
            ("Output", InstanceField.Ty (_Output T));
            ("get", InstanceField.Method (get T));
            ("get_mut", InstanceField.Method (get_mut T));
            ("get_unchecked", InstanceField.Method (get_unchecked T));
            ("get_unchecked_mut", InstanceField.Method (get_unchecked_mut T));
            ("index", InstanceField.Method (index T));
            ("index_mut", InstanceField.Method (index_mut T))
          ].
    End Impl_core_slice_index_SliceIndex_slice_T_for_core_ops_range_RangeFull.
    
    Module Impl_core_slice_index_SliceIndex_slice_T_for_core_ops_range_RangeInclusive_usize.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ].
      
      (*     type Output = [T]; *)
      Definition _Output (T : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ T ].
      
      (*
          fn get(self, slice: &[T]) -> Option<&[T]> {
              if *self.end() == usize::MAX { None } else { self.into_slice_range().get(slice) }
          }
      *)
      Definition get (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.eq (|
                              M.read (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::ops::range::RangeInclusive")
                                      []
                                      [ Ty.path "usize" ],
                                    "end",
                                    []
                                  |),
                                  [ self ]
                                |)
                              |),
                              M.read (| M.get_constant (| "core::num::MAX" |) |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::slice::index::SliceIndex",
                            Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                            [ Ty.apply (Ty.path "slice") [] [ T ] ],
                            "get",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::ops::range::RangeInclusive")
                                  []
                                  [ Ty.path "usize" ],
                                "into_slice_range",
                                []
                              |),
                              [ M.read (| self |) ]
                            |);
                            M.read (| slice |)
                          ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn get_mut(self, slice: &mut [T]) -> Option<&mut [T]> {
              if *self.end() == usize::MAX { None } else { self.into_slice_range().get_mut(slice) }
          }
      *)
      Definition get_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.eq (|
                              M.read (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::ops::range::RangeInclusive")
                                      []
                                      [ Ty.path "usize" ],
                                    "end",
                                    []
                                  |),
                                  [ self ]
                                |)
                              |),
                              M.read (| M.get_constant (| "core::num::MAX" |) |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::slice::index::SliceIndex",
                            Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                            [ Ty.apply (Ty.path "slice") [] [ T ] ],
                            "get_mut",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::ops::range::RangeInclusive")
                                  []
                                  [ Ty.path "usize" ],
                                "into_slice_range",
                                []
                              |),
                              [ M.read (| self |) ]
                            |);
                            M.read (| slice |)
                          ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked(self, slice: *const [T]) -> *const [T] {
              // SAFETY: the caller has to uphold the safety contract for `get_unchecked`.
              unsafe { self.into_slice_range().get_unchecked(slice) }
          }
      *)
      Definition get_unchecked
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get_unchecked",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                    "into_slice_range",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked_mut(self, slice: *mut [T]) -> *mut [T] {
              // SAFETY: the caller has to uphold the safety contract for `get_unchecked_mut`.
              unsafe { self.into_slice_range().get_unchecked_mut(slice) }
          }
      *)
      Definition get_unchecked_mut
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get_unchecked_mut",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                    "into_slice_range",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index(self, slice: &[T]) -> &[T] {
              if *self.end() == usize::MAX {
                  slice_end_index_overflow_fail();
              }
              self.into_slice_range().index(slice)
          }
      *)
      Definition index (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.eq (|
                                M.read (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "core::ops::range::RangeInclusive")
                                        []
                                        [ Ty.path "usize" ],
                                      "end",
                                      []
                                    |),
                                    [ self ]
                                  |)
                                |),
                                M.read (| M.get_constant (| "core::num::MAX" |) |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.call_closure (|
                              M.get_function (|
                                "core::slice::index::slice_end_index_overflow_fail",
                                []
                              |),
                              []
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::slice::index::SliceIndex",
                    Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                    [ Ty.apply (Ty.path "slice") [] [ T ] ],
                    "index",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::ops::range::RangeInclusive")
                          []
                          [ Ty.path "usize" ],
                        "into_slice_range",
                        []
                      |),
                      [ M.read (| self |) ]
                    |);
                    M.read (| slice |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index_mut(self, slice: &mut [T]) -> &mut [T] {
              if *self.end() == usize::MAX {
                  slice_end_index_overflow_fail();
              }
              self.into_slice_range().index_mut(slice)
          }
      *)
      Definition index_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.eq (|
                                M.read (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "core::ops::range::RangeInclusive")
                                        []
                                        [ Ty.path "usize" ],
                                      "end",
                                      []
                                    |),
                                    [ self ]
                                  |)
                                |),
                                M.read (| M.get_constant (| "core::num::MAX" |) |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.call_closure (|
                              M.get_function (|
                                "core::slice::index::slice_end_index_overflow_fail",
                                []
                              |),
                              []
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::slice::index::SliceIndex",
                    Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                    [ Ty.apply (Ty.path "slice") [] [ T ] ],
                    "index_mut",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::ops::range::RangeInclusive")
                          []
                          [ Ty.path "usize" ],
                        "into_slice_range",
                        []
                      |),
                      [ M.read (| self |) ]
                    |);
                    M.read (| slice |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::slice::index::SliceIndex"
          (Self T)
          (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "slice") [] [ T ] ]
          (* Instance *)
          [
            ("Output", InstanceField.Ty (_Output T));
            ("get", InstanceField.Method (get T));
            ("get_mut", InstanceField.Method (get_mut T));
            ("get_unchecked", InstanceField.Method (get_unchecked T));
            ("get_unchecked_mut", InstanceField.Method (get_unchecked_mut T));
            ("index", InstanceField.Method (index T));
            ("index_mut", InstanceField.Method (index_mut T))
          ].
    End Impl_core_slice_index_SliceIndex_slice_T_for_core_ops_range_RangeInclusive_usize.
    
    Module Impl_core_slice_index_SliceIndex_slice_T_for_core_range_RangeInclusive_usize.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::range::RangeInclusive") [] [ Ty.path "usize" ].
      
      (*     type Output = [T]; *)
      Definition _Output (T : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ T ].
      
      (*
          fn get(self, slice: &[T]) -> Option<&[T]> {
              ops::RangeInclusive::from(self).get(slice)
          }
      *)
      Definition get (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::From",
                    Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                    [ Ty.apply (Ty.path "core::range::RangeInclusive") [] [ Ty.path "usize" ] ],
                    "from",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn get_mut(self, slice: &mut [T]) -> Option<&mut [T]> {
              ops::RangeInclusive::from(self).get_mut(slice)
          }
      *)
      Definition get_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get_mut",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::From",
                    Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                    [ Ty.apply (Ty.path "core::range::RangeInclusive") [] [ Ty.path "usize" ] ],
                    "from",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked(self, slice: *const [T]) -> *const [T] {
              // SAFETY: the caller has to uphold the safety contract for `get_unchecked`.
              unsafe { ops::RangeInclusive::from(self).get_unchecked(slice) }
          }
      *)
      Definition get_unchecked
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get_unchecked",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::From",
                    Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                    [ Ty.apply (Ty.path "core::range::RangeInclusive") [] [ Ty.path "usize" ] ],
                    "from",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked_mut(self, slice: *mut [T]) -> *mut [T] {
              // SAFETY: the caller has to uphold the safety contract for `get_unchecked_mut`.
              unsafe { ops::RangeInclusive::from(self).get_unchecked_mut(slice) }
          }
      *)
      Definition get_unchecked_mut
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get_unchecked_mut",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::From",
                    Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                    [ Ty.apply (Ty.path "core::range::RangeInclusive") [] [ Ty.path "usize" ] ],
                    "from",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index(self, slice: &[T]) -> &[T] {
              ops::RangeInclusive::from(self).index(slice)
          }
      *)
      Definition index (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "index",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::From",
                    Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                    [ Ty.apply (Ty.path "core::range::RangeInclusive") [] [ Ty.path "usize" ] ],
                    "from",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index_mut(self, slice: &mut [T]) -> &mut [T] {
              ops::RangeInclusive::from(self).index_mut(slice)
          }
      *)
      Definition index_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "index_mut",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::From",
                    Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                    [ Ty.apply (Ty.path "core::range::RangeInclusive") [] [ Ty.path "usize" ] ],
                    "from",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::slice::index::SliceIndex"
          (Self T)
          (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "slice") [] [ T ] ]
          (* Instance *)
          [
            ("Output", InstanceField.Ty (_Output T));
            ("get", InstanceField.Method (get T));
            ("get_mut", InstanceField.Method (get_mut T));
            ("get_unchecked", InstanceField.Method (get_unchecked T));
            ("get_unchecked_mut", InstanceField.Method (get_unchecked_mut T));
            ("index", InstanceField.Method (index T));
            ("index_mut", InstanceField.Method (index_mut T))
          ].
    End Impl_core_slice_index_SliceIndex_slice_T_for_core_range_RangeInclusive_usize.
    
    Module Impl_core_slice_index_SliceIndex_slice_T_for_core_ops_range_RangeToInclusive_usize.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::range::RangeToInclusive") [] [ Ty.path "usize" ].
      
      (*     type Output = [T]; *)
      Definition _Output (T : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ T ].
      
      (*
          fn get(self, slice: &[T]) -> Option<&[T]> {
              (0..=self.end).get(slice)
          }
      *)
      Definition get (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                    "new",
                    []
                  |),
                  [
                    Value.Integer IntegerKind.Usize 0;
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        self,
                        "core::ops::range::RangeToInclusive",
                        "end"
                      |)
                    |)
                  ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn get_mut(self, slice: &mut [T]) -> Option<&mut [T]> {
              (0..=self.end).get_mut(slice)
          }
      *)
      Definition get_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get_mut",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                    "new",
                    []
                  |),
                  [
                    Value.Integer IntegerKind.Usize 0;
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        self,
                        "core::ops::range::RangeToInclusive",
                        "end"
                      |)
                    |)
                  ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked(self, slice: *const [T]) -> *const [T] {
              // SAFETY: the caller has to uphold the safety contract for `get_unchecked`.
              unsafe { (0..=self.end).get_unchecked(slice) }
          }
      *)
      Definition get_unchecked
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get_unchecked",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                    "new",
                    []
                  |),
                  [
                    Value.Integer IntegerKind.Usize 0;
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        self,
                        "core::ops::range::RangeToInclusive",
                        "end"
                      |)
                    |)
                  ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked_mut(self, slice: *mut [T]) -> *mut [T] {
              // SAFETY: the caller has to uphold the safety contract for `get_unchecked_mut`.
              unsafe { (0..=self.end).get_unchecked_mut(slice) }
          }
      *)
      Definition get_unchecked_mut
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get_unchecked_mut",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                    "new",
                    []
                  |),
                  [
                    Value.Integer IntegerKind.Usize 0;
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        self,
                        "core::ops::range::RangeToInclusive",
                        "end"
                      |)
                    |)
                  ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index(self, slice: &[T]) -> &[T] {
              (0..=self.end).index(slice)
          }
      *)
      Definition index (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "index",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                    "new",
                    []
                  |),
                  [
                    Value.Integer IntegerKind.Usize 0;
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        self,
                        "core::ops::range::RangeToInclusive",
                        "end"
                      |)
                    |)
                  ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index_mut(self, slice: &mut [T]) -> &mut [T] {
              (0..=self.end).index_mut(slice)
          }
      *)
      Definition index_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "index_mut",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                    "new",
                    []
                  |),
                  [
                    Value.Integer IntegerKind.Usize 0;
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        self,
                        "core::ops::range::RangeToInclusive",
                        "end"
                      |)
                    |)
                  ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::slice::index::SliceIndex"
          (Self T)
          (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "slice") [] [ T ] ]
          (* Instance *)
          [
            ("Output", InstanceField.Ty (_Output T));
            ("get", InstanceField.Method (get T));
            ("get_mut", InstanceField.Method (get_mut T));
            ("get_unchecked", InstanceField.Method (get_unchecked T));
            ("get_unchecked_mut", InstanceField.Method (get_unchecked_mut T));
            ("index", InstanceField.Method (index T));
            ("index_mut", InstanceField.Method (index_mut T))
          ].
    End Impl_core_slice_index_SliceIndex_slice_T_for_core_ops_range_RangeToInclusive_usize.
    
    (*
    pub fn range<R>(range: R, bounds: ops::RangeTo<usize>) -> ops::Range<usize>
    where
        R: ops::RangeBounds<usize>,
    {
        let len = bounds.end;
    
        let start = match range.start_bound() {
            ops::Bound::Included(&start) => start,
            ops::Bound::Excluded(start) => {
                start.checked_add(1).unwrap_or_else(|| slice_start_index_overflow_fail())
            }
            ops::Bound::Unbounded => 0,
        };
    
        let end = match range.end_bound() {
            ops::Bound::Included(end) => {
                end.checked_add(1).unwrap_or_else(|| slice_end_index_overflow_fail())
            }
            ops::Bound::Excluded(&end) => end,
            ops::Bound::Unbounded => len,
        };
    
        if start > end {
            slice_index_order_fail(start, end);
        }
        if end > len {
            slice_end_index_len_fail(end, len);
        }
    
        ops::Range { start, end }
    }
    *)
    Definition range (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ R ], [ range; bounds ] =>
        ltac:(M.monadic
          (let range := M.alloc (| range |) in
          let bounds := M.alloc (| bounds |) in
          M.read (|
            let~ len :=
              M.copy (|
                M.SubPointer.get_struct_record_field (|
                  bounds,
                  "core::ops::range::RangeTo",
                  "end"
                |)
              |) in
            let~ start :=
              M.copy (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::range::RangeBounds",
                        R,
                        [ Ty.path "usize" ],
                        "start_bound",
                        []
                      |),
                      [ range ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::range::Bound::Included",
                            0
                          |) in
                        let γ0_0 := M.read (| γ0_0 |) in
                        let start := M.copy (| γ0_0 |) in
                        start));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::range::Bound::Excluded",
                            0
                          |) in
                        let start := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "usize" ],
                              "unwrap_or_else",
                              [ Ty.function [ Ty.tuple [] ] (Ty.path "usize") ]
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (| Ty.path "usize", "checked_add", [] |),
                                [ M.read (| M.read (| start |) |); Value.Integer IntegerKind.Usize 1
                                ]
                              |);
                              M.closure
                                (fun γ =>
                                  ltac:(M.monadic
                                    match γ with
                                    | [ α0 ] =>
                                      ltac:(M.monadic
                                        (M.match_operator (|
                                          M.alloc (| α0 |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (M.never_to_any (|
                                                  M.call_closure (|
                                                    M.get_function (|
                                                      "core::slice::index::slice_start_index_overflow_fail",
                                                      []
                                                    |),
                                                    []
                                                  |)
                                                |)))
                                          ]
                                        |)))
                                    | _ => M.impossible "wrong number of arguments"
                                    end))
                            ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ := M.is_struct_tuple (| γ, "core::ops::range::Bound::Unbounded" |) in
                        M.alloc (| Value.Integer IntegerKind.Usize 0 |)))
                  ]
                |)
              |) in
            let~ end_ :=
              M.copy (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::range::RangeBounds",
                        R,
                        [ Ty.path "usize" ],
                        "end_bound",
                        []
                      |),
                      [ range ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::range::Bound::Included",
                            0
                          |) in
                        let end_ := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "usize" ],
                              "unwrap_or_else",
                              [ Ty.function [ Ty.tuple [] ] (Ty.path "usize") ]
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (| Ty.path "usize", "checked_add", [] |),
                                [ M.read (| M.read (| end_ |) |); Value.Integer IntegerKind.Usize 1
                                ]
                              |);
                              M.closure
                                (fun γ =>
                                  ltac:(M.monadic
                                    match γ with
                                    | [ α0 ] =>
                                      ltac:(M.monadic
                                        (M.match_operator (|
                                          M.alloc (| α0 |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (M.never_to_any (|
                                                  M.call_closure (|
                                                    M.get_function (|
                                                      "core::slice::index::slice_end_index_overflow_fail",
                                                      []
                                                    |),
                                                    []
                                                  |)
                                                |)))
                                          ]
                                        |)))
                                    | _ => M.impossible "wrong number of arguments"
                                    end))
                            ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::range::Bound::Excluded",
                            0
                          |) in
                        let γ0_0 := M.read (| γ0_0 |) in
                        let end_ := M.copy (| γ0_0 |) in
                        end_));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ := M.is_struct_tuple (| γ, "core::ops::range::Bound::Unbounded" |) in
                        len))
                  ]
                |)
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (| BinOp.gt (| M.read (| start |), M.read (| end_ |) |) |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.never_to_any (|
                          M.call_closure (|
                            M.get_function (| "core::slice::index::slice_index_order_fail", [] |),
                            [ M.read (| start |); M.read (| end_ |) ]
                          |)
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use (M.alloc (| BinOp.gt (| M.read (| end_ |), M.read (| len |) |) |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.never_to_any (|
                          M.call_closure (|
                            M.get_function (| "core::slice::index::slice_end_index_len_fail", [] |),
                            [ M.read (| end_ |); M.read (| len |) ]
                          |)
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            M.alloc (|
              Value.StructRecord
                "core::ops::range::Range"
                [ ("start", M.read (| start |)); ("end_", M.read (| end_ |)) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_range : M.IsFunction "core::slice::index::range" range.
    
    (*
    pub fn try_range<R>(range: R, bounds: ops::RangeTo<usize>) -> Option<ops::Range<usize>>
    where
        R: ops::RangeBounds<usize>,
    {
        let len = bounds.end;
    
        let start = match range.start_bound() {
            ops::Bound::Included(&start) => start,
            ops::Bound::Excluded(start) => start.checked_add(1)?,
            ops::Bound::Unbounded => 0,
        };
    
        let end = match range.end_bound() {
            ops::Bound::Included(end) => end.checked_add(1)?,
            ops::Bound::Excluded(&end) => end,
            ops::Bound::Unbounded => len,
        };
    
        if start > end || end > len { None } else { Some(ops::Range { start, end }) }
    }
    *)
    Definition try_range (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ R ], [ range; bounds ] =>
        ltac:(M.monadic
          (let range := M.alloc (| range |) in
          let bounds := M.alloc (| bounds |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ len :=
                  M.copy (|
                    M.SubPointer.get_struct_record_field (|
                      bounds,
                      "core::ops::range::RangeTo",
                      "end"
                    |)
                  |) in
                let~ start :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::range::RangeBounds",
                            R,
                            [ Ty.path "usize" ],
                            "start_bound",
                            []
                          |),
                          [ range ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::range::Bound::Included",
                                0
                              |) in
                            let γ0_0 := M.read (| γ0_0 |) in
                            let start := M.copy (| γ0_0 |) in
                            start));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::range::Bound::Excluded",
                                0
                              |) in
                            let start := M.copy (| γ0_0 |) in
                            M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::try_trait::Try",
                                    Ty.apply
                                      (Ty.path "core::option::Option")
                                      []
                                      [ Ty.path "usize" ],
                                    [],
                                    "branch",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "usize",
                                        "checked_add",
                                        []
                                      |),
                                      [
                                        M.read (| M.read (| start |) |);
                                        Value.Integer IntegerKind.Usize 1
                                      ]
                                    |)
                                  ]
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "core::ops::control_flow::ControlFlow::Break",
                                        0
                                      |) in
                                    let residual := M.copy (| γ0_0 |) in
                                    M.alloc (|
                                      M.never_to_any (|
                                        M.read (|
                                          M.return_ (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::try_trait::FromResidual",
                                                Ty.apply
                                                  (Ty.path "core::option::Option")
                                                  []
                                                  [
                                                    Ty.apply
                                                      (Ty.path "core::ops::range::Range")
                                                      []
                                                      [ Ty.path "usize" ]
                                                  ],
                                                [
                                                  Ty.apply
                                                    (Ty.path "core::option::Option")
                                                    []
                                                    [ Ty.path "core::convert::Infallible" ]
                                                ],
                                                "from_residual",
                                                []
                                              |),
                                              [ M.read (| residual |) ]
                                            |)
                                          |)
                                        |)
                                      |)
                                    |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "core::ops::control_flow::ControlFlow::Continue",
                                        0
                                      |) in
                                    let val := M.copy (| γ0_0 |) in
                                    val))
                              ]
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (| γ, "core::ops::range::Bound::Unbounded" |) in
                            M.alloc (| Value.Integer IntegerKind.Usize 0 |)))
                      ]
                    |)
                  |) in
                let~ end_ :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::range::RangeBounds",
                            R,
                            [ Ty.path "usize" ],
                            "end_bound",
                            []
                          |),
                          [ range ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::range::Bound::Included",
                                0
                              |) in
                            let end_ := M.copy (| γ0_0 |) in
                            M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::try_trait::Try",
                                    Ty.apply
                                      (Ty.path "core::option::Option")
                                      []
                                      [ Ty.path "usize" ],
                                    [],
                                    "branch",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "usize",
                                        "checked_add",
                                        []
                                      |),
                                      [
                                        M.read (| M.read (| end_ |) |);
                                        Value.Integer IntegerKind.Usize 1
                                      ]
                                    |)
                                  ]
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "core::ops::control_flow::ControlFlow::Break",
                                        0
                                      |) in
                                    let residual := M.copy (| γ0_0 |) in
                                    M.alloc (|
                                      M.never_to_any (|
                                        M.read (|
                                          M.return_ (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::try_trait::FromResidual",
                                                Ty.apply
                                                  (Ty.path "core::option::Option")
                                                  []
                                                  [
                                                    Ty.apply
                                                      (Ty.path "core::ops::range::Range")
                                                      []
                                                      [ Ty.path "usize" ]
                                                  ],
                                                [
                                                  Ty.apply
                                                    (Ty.path "core::option::Option")
                                                    []
                                                    [ Ty.path "core::convert::Infallible" ]
                                                ],
                                                "from_residual",
                                                []
                                              |),
                                              [ M.read (| residual |) ]
                                            |)
                                          |)
                                        |)
                                      |)
                                    |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "core::ops::control_flow::ControlFlow::Continue",
                                        0
                                      |) in
                                    let val := M.copy (| γ0_0 |) in
                                    val))
                              ]
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::range::Bound::Excluded",
                                0
                              |) in
                            let γ0_0 := M.read (| γ0_0 |) in
                            let end_ := M.copy (| γ0_0 |) in
                            end_));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (| γ, "core::ops::range::Bound::Unbounded" |) in
                            len))
                      ]
                    |)
                  |) in
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              LogicalOp.or (|
                                BinOp.gt (| M.read (| start |), M.read (| end_ |) |),
                                ltac:(M.monadic
                                  (BinOp.gt (| M.read (| end_ |), M.read (| len |) |)))
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          Value.StructTuple
                            "core::option::Option::Some"
                            [
                              Value.StructRecord
                                "core::ops::range::Range"
                                [ ("start", M.read (| start |)); ("end_", M.read (| end_ |)) ]
                            ]
                        |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_try_range : M.IsFunction "core::slice::index::try_range" try_range.
    
    (*
    pub(crate) fn into_range_unchecked(
        len: usize,
        (start, end): (ops::Bound<usize>, ops::Bound<usize>),
    ) -> ops::Range<usize> {
        use ops::Bound;
        let start = match start {
            Bound::Included(i) => i,
            Bound::Excluded(i) => i + 1,
            Bound::Unbounded => 0,
        };
        let end = match end {
            Bound::Included(i) => i + 1,
            Bound::Excluded(i) => i,
            Bound::Unbounded => len,
        };
        start..end
    }
    *)
    Definition into_range_unchecked (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ len; β1 ] =>
        ltac:(M.monadic
          (let len := M.alloc (| len |) in
          let β1 := M.alloc (| β1 |) in
          M.match_operator (|
            β1,
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                  let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                  let start := M.copy (| γ0_0 |) in
                  let end_ := M.copy (| γ0_1 |) in
                  M.read (|
                    let~ start :=
                      M.copy (|
                        M.match_operator (|
                          start,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::range::Bound::Included",
                                    0
                                  |) in
                                let i := M.copy (| γ0_0 |) in
                                i));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::range::Bound::Excluded",
                                    0
                                  |) in
                                let i := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  BinOp.Wrap.add (|
                                    M.read (| i |),
                                    Value.Integer IntegerKind.Usize 1
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ :=
                                  M.is_struct_tuple (| γ, "core::ops::range::Bound::Unbounded" |) in
                                M.alloc (| Value.Integer IntegerKind.Usize 0 |)))
                          ]
                        |)
                      |) in
                    let~ end_ :=
                      M.copy (|
                        M.match_operator (|
                          end_,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::range::Bound::Included",
                                    0
                                  |) in
                                let i := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  BinOp.Wrap.add (|
                                    M.read (| i |),
                                    Value.Integer IntegerKind.Usize 1
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::range::Bound::Excluded",
                                    0
                                  |) in
                                let i := M.copy (| γ0_0 |) in
                                i));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ :=
                                  M.is_struct_tuple (| γ, "core::ops::range::Bound::Unbounded" |) in
                                len))
                          ]
                        |)
                      |) in
                    M.alloc (|
                      Value.StructRecord
                        "core::ops::range::Range"
                        [ ("start", M.read (| start |)); ("end_", M.read (| end_ |)) ]
                    |)
                  |)))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_into_range_unchecked :
      M.IsFunction "core::slice::index::into_range_unchecked" into_range_unchecked.
    
    (*
    pub(crate) fn into_range(
        len: usize,
        (start, end): (ops::Bound<usize>, ops::Bound<usize>),
    ) -> Option<ops::Range<usize>> {
        use ops::Bound;
        let start = match start {
            Bound::Included(start) => start,
            Bound::Excluded(start) => start.checked_add(1)?,
            Bound::Unbounded => 0,
        };
    
        let end = match end {
            Bound::Included(end) => end.checked_add(1)?,
            Bound::Excluded(end) => end,
            Bound::Unbounded => len,
        };
    
        // Don't bother with checking `start < end` and `end <= len`
        // since these checks are handled by `Range` impls
    
        Some(start..end)
    }
    *)
    Definition into_range (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ len; β1 ] =>
        ltac:(M.monadic
          (let len := M.alloc (| len |) in
          let β1 := M.alloc (| β1 |) in
          M.match_operator (|
            β1,
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                  let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                  let start := M.copy (| γ0_0 |) in
                  let end_ := M.copy (| γ0_1 |) in
                  M.catch_return (|
                    ltac:(M.monadic
                      (M.read (|
                        let~ start :=
                          M.copy (|
                            M.match_operator (|
                              start,
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "core::ops::range::Bound::Included",
                                        0
                                      |) in
                                    let start := M.copy (| γ0_0 |) in
                                    start));
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "core::ops::range::Bound::Excluded",
                                        0
                                      |) in
                                    let start := M.copy (| γ0_0 |) in
                                    M.match_operator (|
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::Try",
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "usize" ],
                                            [],
                                            "branch",
                                            []
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "usize",
                                                "checked_add",
                                                []
                                              |),
                                              [
                                                M.read (| start |);
                                                Value.Integer IntegerKind.Usize 1
                                              ]
                                            |)
                                          ]
                                        |)
                                      |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ0_0 :=
                                              M.SubPointer.get_struct_tuple_field (|
                                                γ,
                                                "core::ops::control_flow::ControlFlow::Break",
                                                0
                                              |) in
                                            let residual := M.copy (| γ0_0 |) in
                                            M.alloc (|
                                              M.never_to_any (|
                                                M.read (|
                                                  M.return_ (|
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::ops::try_trait::FromResidual",
                                                        Ty.apply
                                                          (Ty.path "core::option::Option")
                                                          []
                                                          [
                                                            Ty.apply
                                                              (Ty.path "core::ops::range::Range")
                                                              []
                                                              [ Ty.path "usize" ]
                                                          ],
                                                        [
                                                          Ty.apply
                                                            (Ty.path "core::option::Option")
                                                            []
                                                            [ Ty.path "core::convert::Infallible" ]
                                                        ],
                                                        "from_residual",
                                                        []
                                                      |),
                                                      [ M.read (| residual |) ]
                                                    |)
                                                  |)
                                                |)
                                              |)
                                            |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ0_0 :=
                                              M.SubPointer.get_struct_tuple_field (|
                                                γ,
                                                "core::ops::control_flow::ControlFlow::Continue",
                                                0
                                              |) in
                                            let val := M.copy (| γ0_0 |) in
                                            val))
                                      ]
                                    |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (let _ :=
                                      M.is_struct_tuple (|
                                        γ,
                                        "core::ops::range::Bound::Unbounded"
                                      |) in
                                    M.alloc (| Value.Integer IntegerKind.Usize 0 |)))
                              ]
                            |)
                          |) in
                        let~ end_ :=
                          M.copy (|
                            M.match_operator (|
                              end_,
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "core::ops::range::Bound::Included",
                                        0
                                      |) in
                                    let end_ := M.copy (| γ0_0 |) in
                                    M.match_operator (|
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::Try",
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "usize" ],
                                            [],
                                            "branch",
                                            []
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "usize",
                                                "checked_add",
                                                []
                                              |),
                                              [ M.read (| end_ |); Value.Integer IntegerKind.Usize 1
                                              ]
                                            |)
                                          ]
                                        |)
                                      |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ0_0 :=
                                              M.SubPointer.get_struct_tuple_field (|
                                                γ,
                                                "core::ops::control_flow::ControlFlow::Break",
                                                0
                                              |) in
                                            let residual := M.copy (| γ0_0 |) in
                                            M.alloc (|
                                              M.never_to_any (|
                                                M.read (|
                                                  M.return_ (|
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::ops::try_trait::FromResidual",
                                                        Ty.apply
                                                          (Ty.path "core::option::Option")
                                                          []
                                                          [
                                                            Ty.apply
                                                              (Ty.path "core::ops::range::Range")
                                                              []
                                                              [ Ty.path "usize" ]
                                                          ],
                                                        [
                                                          Ty.apply
                                                            (Ty.path "core::option::Option")
                                                            []
                                                            [ Ty.path "core::convert::Infallible" ]
                                                        ],
                                                        "from_residual",
                                                        []
                                                      |),
                                                      [ M.read (| residual |) ]
                                                    |)
                                                  |)
                                                |)
                                              |)
                                            |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ0_0 :=
                                              M.SubPointer.get_struct_tuple_field (|
                                                γ,
                                                "core::ops::control_flow::ControlFlow::Continue",
                                                0
                                              |) in
                                            let val := M.copy (| γ0_0 |) in
                                            val))
                                      ]
                                    |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "core::ops::range::Bound::Excluded",
                                        0
                                      |) in
                                    let end_ := M.copy (| γ0_0 |) in
                                    end_));
                                fun γ =>
                                  ltac:(M.monadic
                                    (let _ :=
                                      M.is_struct_tuple (|
                                        γ,
                                        "core::ops::range::Bound::Unbounded"
                                      |) in
                                    len))
                              ]
                            |)
                          |) in
                        M.alloc (|
                          Value.StructTuple
                            "core::option::Option::Some"
                            [
                              Value.StructRecord
                                "core::ops::range::Range"
                                [ ("start", M.read (| start |)); ("end_", M.read (| end_ |)) ]
                            ]
                        |)
                      |)))
                  |)))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_into_range : M.IsFunction "core::slice::index::into_range" into_range.
    
    (*
    pub(crate) fn into_slice_range(
        len: usize,
        (start, end): (ops::Bound<usize>, ops::Bound<usize>),
    ) -> ops::Range<usize> {
        use ops::Bound;
        let start = match start {
            Bound::Included(start) => start,
            Bound::Excluded(start) => {
                start.checked_add(1).unwrap_or_else(|| slice_start_index_overflow_fail())
            }
            Bound::Unbounded => 0,
        };
    
        let end = match end {
            Bound::Included(end) => {
                end.checked_add(1).unwrap_or_else(|| slice_end_index_overflow_fail())
            }
            Bound::Excluded(end) => end,
            Bound::Unbounded => len,
        };
    
        // Don't bother with checking `start < end` and `end <= len`
        // since these checks are handled by `Range` impls
    
        start..end
    }
    *)
    Definition into_slice_range (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ len; β1 ] =>
        ltac:(M.monadic
          (let len := M.alloc (| len |) in
          let β1 := M.alloc (| β1 |) in
          M.match_operator (|
            β1,
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                  let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                  let start := M.copy (| γ0_0 |) in
                  let end_ := M.copy (| γ0_1 |) in
                  M.read (|
                    let~ start :=
                      M.copy (|
                        M.match_operator (|
                          start,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::range::Bound::Included",
                                    0
                                  |) in
                                let start := M.copy (| γ0_0 |) in
                                start));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::range::Bound::Excluded",
                                    0
                                  |) in
                                let start := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "core::option::Option")
                                        []
                                        [ Ty.path "usize" ],
                                      "unwrap_or_else",
                                      [ Ty.function [ Ty.tuple [] ] (Ty.path "usize") ]
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "usize",
                                          "checked_add",
                                          []
                                        |),
                                        [ M.read (| start |); Value.Integer IntegerKind.Usize 1 ]
                                      |);
                                      M.closure
                                        (fun γ =>
                                          ltac:(M.monadic
                                            match γ with
                                            | [ α0 ] =>
                                              ltac:(M.monadic
                                                (M.match_operator (|
                                                  M.alloc (| α0 |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (M.never_to_any (|
                                                          M.call_closure (|
                                                            M.get_function (|
                                                              "core::slice::index::slice_start_index_overflow_fail",
                                                              []
                                                            |),
                                                            []
                                                          |)
                                                        |)))
                                                  ]
                                                |)))
                                            | _ => M.impossible "wrong number of arguments"
                                            end))
                                    ]
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ :=
                                  M.is_struct_tuple (| γ, "core::ops::range::Bound::Unbounded" |) in
                                M.alloc (| Value.Integer IntegerKind.Usize 0 |)))
                          ]
                        |)
                      |) in
                    let~ end_ :=
                      M.copy (|
                        M.match_operator (|
                          end_,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::range::Bound::Included",
                                    0
                                  |) in
                                let end_ := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "core::option::Option")
                                        []
                                        [ Ty.path "usize" ],
                                      "unwrap_or_else",
                                      [ Ty.function [ Ty.tuple [] ] (Ty.path "usize") ]
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "usize",
                                          "checked_add",
                                          []
                                        |),
                                        [ M.read (| end_ |); Value.Integer IntegerKind.Usize 1 ]
                                      |);
                                      M.closure
                                        (fun γ =>
                                          ltac:(M.monadic
                                            match γ with
                                            | [ α0 ] =>
                                              ltac:(M.monadic
                                                (M.match_operator (|
                                                  M.alloc (| α0 |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (M.never_to_any (|
                                                          M.call_closure (|
                                                            M.get_function (|
                                                              "core::slice::index::slice_end_index_overflow_fail",
                                                              []
                                                            |),
                                                            []
                                                          |)
                                                        |)))
                                                  ]
                                                |)))
                                            | _ => M.impossible "wrong number of arguments"
                                            end))
                                    ]
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::range::Bound::Excluded",
                                    0
                                  |) in
                                let end_ := M.copy (| γ0_0 |) in
                                end_));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ :=
                                  M.is_struct_tuple (| γ, "core::ops::range::Bound::Unbounded" |) in
                                len))
                          ]
                        |)
                      |) in
                    M.alloc (|
                      Value.StructRecord
                        "core::ops::range::Range"
                        [ ("start", M.read (| start |)); ("end_", M.read (| end_ |)) ]
                    |)
                  |)))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_into_slice_range :
      M.IsFunction "core::slice::index::into_slice_range" into_slice_range.
    
    Module Impl_core_slice_index_SliceIndex_slice_T_for_Tuple_core_ops_range_Bound_usize_core_ops_range_Bound_usize_.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.tuple
          [
            Ty.apply (Ty.path "core::ops::range::Bound") [] [ Ty.path "usize" ];
            Ty.apply (Ty.path "core::ops::range::Bound") [] [ Ty.path "usize" ]
          ].
      
      (*     type Output = [T]; *)
      Definition _Output (T : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ T ].
      
      (*
          fn get(self, slice: &[T]) -> Option<&Self::Output> {
              into_range(slice.len(), self)?.get(slice)
          }
      *)
      Definition get (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_trait_method (|
                    "core::slice::index::SliceIndex",
                    Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                    [ Ty.apply (Ty.path "slice") [] [ T ] ],
                    "get",
                    []
                  |),
                  [
                    M.read (|
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::try_trait::Try",
                              Ty.apply
                                (Ty.path "core::option::Option")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "core::ops::range::Range")
                                    []
                                    [ Ty.path "usize" ]
                                ],
                              [],
                              "branch",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_function (| "core::slice::index::into_range", [] |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "slice") [] [ T ],
                                      "len",
                                      []
                                    |),
                                    [ M.read (| slice |) ]
                                  |);
                                  M.read (| self |)
                                ]
                              |)
                            ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::ops::control_flow::ControlFlow::Break",
                                  0
                                |) in
                              let residual := M.copy (| γ0_0 |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    M.return_ (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::ops::try_trait::FromResidual",
                                          Ty.apply
                                            (Ty.path "core::option::Option")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "&")
                                                []
                                                [ Ty.apply (Ty.path "slice") [] [ T ] ]
                                            ],
                                          [
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "core::convert::Infallible" ]
                                          ],
                                          "from_residual",
                                          []
                                        |),
                                        [ M.read (| residual |) ]
                                      |)
                                    |)
                                  |)
                                |)
                              |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::ops::control_flow::ControlFlow::Continue",
                                  0
                                |) in
                              let val := M.copy (| γ0_0 |) in
                              val))
                        ]
                      |)
                    |);
                    M.read (| slice |)
                  ]
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn get_mut(self, slice: &mut [T]) -> Option<&mut Self::Output> {
              into_range(slice.len(), self)?.get_mut(slice)
          }
      *)
      Definition get_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_trait_method (|
                    "core::slice::index::SliceIndex",
                    Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                    [ Ty.apply (Ty.path "slice") [] [ T ] ],
                    "get_mut",
                    []
                  |),
                  [
                    M.read (|
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::try_trait::Try",
                              Ty.apply
                                (Ty.path "core::option::Option")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "core::ops::range::Range")
                                    []
                                    [ Ty.path "usize" ]
                                ],
                              [],
                              "branch",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_function (| "core::slice::index::into_range", [] |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "slice") [] [ T ],
                                      "len",
                                      []
                                    |),
                                    [ M.read (| slice |) ]
                                  |);
                                  M.read (| self |)
                                ]
                              |)
                            ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::ops::control_flow::ControlFlow::Break",
                                  0
                                |) in
                              let residual := M.copy (| γ0_0 |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    M.return_ (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::ops::try_trait::FromResidual",
                                          Ty.apply
                                            (Ty.path "core::option::Option")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "&mut")
                                                []
                                                [ Ty.apply (Ty.path "slice") [] [ T ] ]
                                            ],
                                          [
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "core::convert::Infallible" ]
                                          ],
                                          "from_residual",
                                          []
                                        |),
                                        [ M.read (| residual |) ]
                                      |)
                                    |)
                                  |)
                                |)
                              |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::ops::control_flow::ControlFlow::Continue",
                                  0
                                |) in
                              let val := M.copy (| γ0_0 |) in
                              val))
                        ]
                      |)
                    |);
                    M.read (| slice |)
                  ]
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked(self, slice: *const [T]) -> *const Self::Output {
              // SAFETY: the caller has to uphold the safety contract for `get_unchecked`.
              unsafe { into_range_unchecked(slice.len(), self).get_unchecked(slice) }
          }
      *)
      Definition get_unchecked
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get_unchecked",
                []
              |),
              [
                M.call_closure (|
                  M.get_function (| "core::slice::index::into_range_unchecked", [] |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "*const") [] [ Ty.apply (Ty.path "slice") [] [ T ] ],
                        "len",
                        []
                      |),
                      [ M.read (| slice |) ]
                    |);
                    M.read (| self |)
                  ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked_mut(self, slice: *mut [T]) -> *mut Self::Output {
              // SAFETY: the caller has to uphold the safety contract for `get_unchecked_mut`.
              unsafe { into_range_unchecked(slice.len(), self).get_unchecked_mut(slice) }
          }
      *)
      Definition get_unchecked_mut
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get_unchecked_mut",
                []
              |),
              [
                M.call_closure (|
                  M.get_function (| "core::slice::index::into_range_unchecked", [] |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "*mut") [] [ Ty.apply (Ty.path "slice") [] [ T ] ],
                        "len",
                        []
                      |),
                      [ M.read (| slice |) ]
                    |);
                    M.read (| self |)
                  ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index(self, slice: &[T]) -> &Self::Output {
              into_slice_range(slice.len(), self).index(slice)
          }
      *)
      Definition index (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "index",
                []
              |),
              [
                M.call_closure (|
                  M.get_function (| "core::slice::index::into_slice_range", [] |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ T ],
                        "len",
                        []
                      |),
                      [ M.read (| slice |) ]
                    |);
                    M.read (| self |)
                  ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index_mut(self, slice: &mut [T]) -> &mut Self::Output {
              into_slice_range(slice.len(), self).index_mut(slice)
          }
      *)
      Definition index_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "index_mut",
                []
              |),
              [
                M.call_closure (|
                  M.get_function (| "core::slice::index::into_slice_range", [] |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ T ],
                        "len",
                        []
                      |),
                      [ M.read (| slice |) ]
                    |);
                    M.read (| self |)
                  ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::slice::index::SliceIndex"
          (Self T)
          (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "slice") [] [ T ] ]
          (* Instance *)
          [
            ("Output", InstanceField.Ty (_Output T));
            ("get", InstanceField.Method (get T));
            ("get_mut", InstanceField.Method (get_mut T));
            ("get_unchecked", InstanceField.Method (get_unchecked T));
            ("get_unchecked_mut", InstanceField.Method (get_unchecked_mut T));
            ("index", InstanceField.Method (index T));
            ("index_mut", InstanceField.Method (index_mut T))
          ].
    End Impl_core_slice_index_SliceIndex_slice_T_for_Tuple_core_ops_range_Bound_usize_core_ops_range_Bound_usize_.
  End index.
End slice.
