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

Module range.
  (* StructRecord
    {
      name := "Range";
      const_params := [];
      ty_params := [ "Idx" ];
      fields := [ ("start", Idx); ("end_", Idx) ];
    } *)
  
  Module Impl_core_clone_Clone_where_core_clone_Clone_Idx_for_core_range_Range_Idx.
    Definition Self (Idx : Ty.t) : Ty.t := Ty.apply (Ty.path "core::range::Range") [] [ Idx ].
    
    (* Clone *)
    Definition clone (Idx : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Idx in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructRecord
            "core::range::Range"
            [
              ("start",
                M.call_closure (|
                  M.get_trait_method (| "core::clone::Clone", Idx, [], "clone", [] |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::range::Range",
                      "start"
                    |)
                  ]
                |));
              ("end_",
                M.call_closure (|
                  M.get_trait_method (| "core::clone::Clone", Idx, [], "clone", [] |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::range::Range",
                      "end"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (Idx : Ty.t),
      M.IsTraitInstance
        "core::clone::Clone"
        (Self Idx)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method (clone Idx)) ].
  End Impl_core_clone_Clone_where_core_clone_Clone_Idx_for_core_range_Range_Idx.
  
  Module Impl_core_marker_Copy_where_core_marker_Copy_Idx_for_core_range_Range_Idx.
    Definition Self (Idx : Ty.t) : Ty.t := Ty.apply (Ty.path "core::range::Range") [] [ Idx ].
    
    Axiom Implements :
      forall (Idx : Ty.t),
      M.IsTraitInstance
        "core::marker::Copy"
        (Self Idx)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_where_core_marker_Copy_Idx_for_core_range_Range_Idx.
  
  Module Impl_core_default_Default_where_core_default_Default_Idx_for_core_range_Range_Idx.
    Definition Self (Idx : Ty.t) : Ty.t := Ty.apply (Ty.path "core::range::Range") [] [ Idx ].
    
    (* Default *)
    Definition default (Idx : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Idx in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructRecord
            "core::range::Range"
            [
              ("start",
                M.call_closure (|
                  M.get_trait_method (| "core::default::Default", Idx, [], "default", [] |),
                  []
                |));
              ("end_",
                M.call_closure (|
                  M.get_trait_method (| "core::default::Default", Idx, [], "default", [] |),
                  []
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (Idx : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self Idx)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default Idx)) ].
  End Impl_core_default_Default_where_core_default_Default_Idx_for_core_range_Range_Idx.
  
  Module Impl_core_marker_StructuralPartialEq_for_core_range_Range_Idx.
    Definition Self (Idx : Ty.t) : Ty.t := Ty.apply (Ty.path "core::range::Range") [] [ Idx ].
    
    Axiom Implements :
      forall (Idx : Ty.t),
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        (Self Idx)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_core_range_Range_Idx.
  
  Module Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_Idx_for_core_range_Range_Idx.
    Definition Self (Idx : Ty.t) : Ty.t := Ty.apply (Ty.path "core::range::Range") [] [ Idx ].
    
    (* PartialEq *)
    Definition eq (Idx : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Idx in
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          LogicalOp.and (|
            M.call_closure (|
              M.get_trait_method (| "core::cmp::PartialEq", Idx, [ Idx ], "eq", [] |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::range::Range",
                  "start"
                |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| other |),
                  "core::range::Range",
                  "start"
                |)
              ]
            |),
            ltac:(M.monadic
              (M.call_closure (|
                M.get_trait_method (| "core::cmp::PartialEq", Idx, [ Idx ], "eq", [] |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::range::Range",
                    "end"
                  |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "core::range::Range",
                    "end"
                  |)
                ]
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (Idx : Ty.t),
      M.IsTraitInstance
        "core::cmp::PartialEq"
        (Self Idx)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method (eq Idx)) ].
  End Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_Idx_for_core_range_Range_Idx.
  
  Module Impl_core_cmp_Eq_where_core_cmp_Eq_Idx_for_core_range_Range_Idx.
    Definition Self (Idx : Ty.t) : Ty.t := Ty.apply (Ty.path "core::range::Range") [] [ Idx ].
    
    (* Eq *)
    Definition assert_receiver_is_total_eq
        (Idx : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self Idx in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (Idx : Ty.t),
      M.IsTraitInstance
        "core::cmp::Eq"
        (Self Idx)
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("assert_receiver_is_total_eq", InstanceField.Method (assert_receiver_is_total_eq Idx)) ].
  End Impl_core_cmp_Eq_where_core_cmp_Eq_Idx_for_core_range_Range_Idx.
  
  Module Impl_core_hash_Hash_where_core_hash_Hash_Idx_for_core_range_Range_Idx.
    Definition Self (Idx : Ty.t) : Ty.t := Ty.apply (Ty.path "core::range::Range") [] [ Idx ].
    
    (* Hash *)
    Definition hash (Idx : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Idx in
      match ε, τ, α with
      | [], [ __H ], [ self; state ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let state := M.alloc (| state |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::hash::Hash", Idx, [], "hash", [ __H ] |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::range::Range",
                      "start"
                    |);
                    M.read (| state |)
                  ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (| "core::hash::Hash", Idx, [], "hash", [ __H ] |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::range::Range",
                    "end"
                  |);
                  M.read (| state |)
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (Idx : Ty.t),
      M.IsTraitInstance
        "core::hash::Hash"
        (Self Idx)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method (hash Idx)) ].
  End Impl_core_hash_Hash_where_core_hash_Hash_Idx_for_core_range_Range_Idx.
  
  Module Impl_core_fmt_Debug_where_core_fmt_Debug_Idx_for_core_range_Range_Idx.
    Definition Self (Idx : Ty.t) : Ty.t := Ty.apply (Ty.path "core::range::Range") [] [ Idx ].
    
    (*
        fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
            self.start.fmt(fmt)?;
            write!(fmt, "..")?;
            self.end.fmt(fmt)?;
            Ok(())
        }
    *)
    Definition fmt (Idx : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Idx in
      match ε, τ, α with
      | [], [], [ self; fmt ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let fmt := M.alloc (| fmt |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::try_trait::Try",
                          Ty.apply
                            (Ty.path "core::result::Result")
                            []
                            [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                          [],
                          "branch",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (| "core::fmt::Debug", Idx, [], "fmt", [] |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::range::Range",
                                "start"
                              |);
                              M.read (| fmt |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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::result::Result")
                                        []
                                        [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                                      [
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [
                                            Ty.path "core::convert::Infallible";
                                            Ty.path "core::fmt::Error"
                                          ]
                                      ],
                                      "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))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::try_trait::Try",
                          Ty.apply
                            (Ty.path "core::result::Result")
                            []
                            [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                          [],
                          "branch",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Formatter",
                              "write_fmt",
                              []
                            |),
                            [
                              M.read (| fmt |);
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::Arguments",
                                  "new_const",
                                  []
                                |),
                                [ M.alloc (| Value.Array [ M.read (| Value.String ".." |) ] |) ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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::result::Result")
                                        []
                                        [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                                      [
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [
                                            Ty.path "core::convert::Infallible";
                                            Ty.path "core::fmt::Error"
                                          ]
                                      ],
                                      "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))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::try_trait::Try",
                          Ty.apply
                            (Ty.path "core::result::Result")
                            []
                            [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                          [],
                          "branch",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (| "core::fmt::Debug", Idx, [], "fmt", [] |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::range::Range",
                                "end"
                              |);
                              M.read (| fmt |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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::result::Result")
                                        []
                                        [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                                      [
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [
                                            Ty.path "core::convert::Infallible";
                                            Ty.path "core::fmt::Error"
                                          ]
                                      ],
                                      "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))
                    ]
                  |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (Idx : Ty.t),
      M.IsTraitInstance
        "core::fmt::Debug"
        (Self Idx)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt Idx)) ].
  End Impl_core_fmt_Debug_where_core_fmt_Debug_Idx_for_core_range_Range_Idx.
  
  Module Impl_core_range_Range_Idx.
    Definition Self (Idx : Ty.t) : Ty.t := Ty.apply (Ty.path "core::range::Range") [] [ Idx ].
    
    (*
        pub fn iter(&self) -> IterRange<Idx> {
            self.clone().into_iter()
        }
    *)
    Definition iter (Idx : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Idx in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::iter::traits::collect::IntoIterator",
              Ty.apply (Ty.path "core::range::Range") [] [ Idx ],
              [],
              "into_iter",
              []
            |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::clone::Clone",
                  Ty.apply (Ty.path "core::range::Range") [] [ Idx ],
                  [],
                  "clone",
                  []
                |),
                [ M.read (| self |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_iter :
      forall (Idx : Ty.t),
      M.IsAssociatedFunction (Self Idx) "iter" (iter Idx).
    (*
        pub fn contains<U>(&self, item: &U) -> bool
        where
            Idx: PartialOrd<U>,
            U: ?Sized + PartialOrd<Idx>,
        {
            <Self as RangeBounds<Idx>>::contains(self, item)
        }
    *)
    Definition contains (Idx : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Idx in
      match ε, τ, α with
      | [], [ U ], [ self; item ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let item := M.alloc (| item |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::ops::range::RangeBounds",
              Ty.apply (Ty.path "core::range::Range") [] [ Idx ],
              [ Idx ],
              "contains",
              [ U ]
            |),
            [ M.read (| self |); M.read (| item |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_contains :
      forall (Idx : Ty.t),
      M.IsAssociatedFunction (Self Idx) "contains" (contains Idx).
    
    (*
        pub fn is_empty(&self) -> bool {
            !(self.start < self.end)
        }
    *)
    Definition is_empty (Idx : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Idx in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          UnOp.not (|
            M.call_closure (|
              M.get_trait_method (| "core::cmp::PartialOrd", Idx, [ Idx ], "lt", [] |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::range::Range",
                  "start"
                |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::range::Range",
                  "end"
                |)
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_empty :
      forall (Idx : Ty.t),
      M.IsAssociatedFunction (Self Idx) "is_empty" (is_empty Idx).
  End Impl_core_range_Range_Idx.
  
  
  Module Impl_core_ops_range_RangeBounds_T_for_core_range_Range_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::range::Range") [] [ T ].
    
    (*
        fn start_bound(&self) -> Bound<&T> {
            Included(&self.start)
        }
    *)
    Definition start_bound (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructTuple
            "core::ops::range::Bound::Included"
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::range::Range",
                "start"
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn end_bound(&self) -> Bound<&T> {
            Excluded(&self.end)
        }
    *)
    Definition end_bound (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructTuple
            "core::ops::range::Bound::Excluded"
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::range::Range",
                "end"
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::ops::range::RangeBounds"
        (Self T)
        (* Trait polymorphic types *) [ (* T *) T ]
        (* Instance *)
        [
          ("start_bound", InstanceField.Method (start_bound T));
          ("end_bound", InstanceField.Method (end_bound T))
        ].
  End Impl_core_ops_range_RangeBounds_T_for_core_range_Range_T.
  
  Module Impl_core_ops_range_RangeBounds_T_for_core_range_Range_ref__T.
    Definition Self (T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::range::Range") [] [ Ty.apply (Ty.path "&") [] [ T ] ].
    
    (*
        fn start_bound(&self) -> Bound<&T> {
            Included(self.start)
        }
    *)
    Definition start_bound (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructTuple
            "core::ops::range::Bound::Included"
            [
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::range::Range",
                  "start"
                |)
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn end_bound(&self) -> Bound<&T> {
            Excluded(self.end)
        }
    *)
    Definition end_bound (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructTuple
            "core::ops::range::Bound::Excluded"
            [
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::range::Range",
                  "end"
                |)
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::ops::range::RangeBounds"
        (Self T)
        (* Trait polymorphic types *) [ (* T *) T ]
        (* Instance *)
        [
          ("start_bound", InstanceField.Method (start_bound T));
          ("end_bound", InstanceField.Method (end_bound T))
        ].
  End Impl_core_ops_range_RangeBounds_T_for_core_range_Range_ref__T.
  
  Module Impl_core_convert_From_core_range_Range_T_for_core_ops_range_Range_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::ops::range::Range") [] [ T ].
    
    (*
        fn from(value: Range<T>) -> Self {
            Self { start: value.start, end: value.end }
        }
    *)
    Definition from (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ value ] =>
        ltac:(M.monadic
          (let value := M.alloc (| value |) in
          Value.StructRecord
            "core::ops::range::Range"
            [
              ("start",
                M.read (|
                  M.SubPointer.get_struct_record_field (| value, "core::range::Range", "start" |)
                |));
              ("end_",
                M.read (|
                  M.SubPointer.get_struct_record_field (| value, "core::range::Range", "end" |)
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::convert::From"
        (Self T)
        (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "core::range::Range") [] [ T ] ]
        (* Instance *) [ ("from", InstanceField.Method (from T)) ].
  End Impl_core_convert_From_core_range_Range_T_for_core_ops_range_Range_T.
  
  Module Impl_core_convert_From_core_ops_range_Range_T_for_core_range_Range_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::range::Range") [] [ T ].
    
    (*
        fn from(value: legacy::Range<T>) -> Self {
            Self { start: value.start, end: value.end }
        }
    *)
    Definition from (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ value ] =>
        ltac:(M.monadic
          (let value := M.alloc (| value |) in
          Value.StructRecord
            "core::range::Range"
            [
              ("start",
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    value,
                    "core::ops::range::Range",
                    "start"
                  |)
                |));
              ("end_",
                M.read (|
                  M.SubPointer.get_struct_record_field (| value, "core::ops::range::Range", "end" |)
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::convert::From"
        (Self T)
        (* Trait polymorphic types *)
        [ (* T *) Ty.apply (Ty.path "core::ops::range::Range") [] [ T ] ]
        (* Instance *) [ ("from", InstanceField.Method (from T)) ].
  End Impl_core_convert_From_core_ops_range_Range_T_for_core_range_Range_T.
  
  (* StructRecord
    {
      name := "RangeInclusive";
      const_params := [];
      ty_params := [ "Idx" ];
      fields := [ ("start", Idx); ("end_", Idx) ];
    } *)
  
  Module Impl_core_clone_Clone_where_core_clone_Clone_Idx_for_core_range_RangeInclusive_Idx.
    Definition Self (Idx : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::range::RangeInclusive") [] [ Idx ].
    
    (* Clone *)
    Definition clone (Idx : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Idx in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructRecord
            "core::range::RangeInclusive"
            [
              ("start",
                M.call_closure (|
                  M.get_trait_method (| "core::clone::Clone", Idx, [], "clone", [] |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::range::RangeInclusive",
                      "start"
                    |)
                  ]
                |));
              ("end_",
                M.call_closure (|
                  M.get_trait_method (| "core::clone::Clone", Idx, [], "clone", [] |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::range::RangeInclusive",
                      "end"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (Idx : Ty.t),
      M.IsTraitInstance
        "core::clone::Clone"
        (Self Idx)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method (clone Idx)) ].
  End Impl_core_clone_Clone_where_core_clone_Clone_Idx_for_core_range_RangeInclusive_Idx.
  
  Module Impl_core_marker_Copy_where_core_marker_Copy_Idx_for_core_range_RangeInclusive_Idx.
    Definition Self (Idx : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::range::RangeInclusive") [] [ Idx ].
    
    Axiom Implements :
      forall (Idx : Ty.t),
      M.IsTraitInstance
        "core::marker::Copy"
        (Self Idx)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_where_core_marker_Copy_Idx_for_core_range_RangeInclusive_Idx.
  
  Module Impl_core_marker_StructuralPartialEq_for_core_range_RangeInclusive_Idx.
    Definition Self (Idx : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::range::RangeInclusive") [] [ Idx ].
    
    Axiom Implements :
      forall (Idx : Ty.t),
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        (Self Idx)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_core_range_RangeInclusive_Idx.
  
  Module Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_Idx_for_core_range_RangeInclusive_Idx.
    Definition Self (Idx : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::range::RangeInclusive") [] [ Idx ].
    
    (* PartialEq *)
    Definition eq (Idx : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Idx in
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          LogicalOp.and (|
            M.call_closure (|
              M.get_trait_method (| "core::cmp::PartialEq", Idx, [ Idx ], "eq", [] |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::range::RangeInclusive",
                  "start"
                |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| other |),
                  "core::range::RangeInclusive",
                  "start"
                |)
              ]
            |),
            ltac:(M.monadic
              (M.call_closure (|
                M.get_trait_method (| "core::cmp::PartialEq", Idx, [ Idx ], "eq", [] |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::range::RangeInclusive",
                    "end"
                  |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "core::range::RangeInclusive",
                    "end"
                  |)
                ]
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (Idx : Ty.t),
      M.IsTraitInstance
        "core::cmp::PartialEq"
        (Self Idx)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method (eq Idx)) ].
  End Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_Idx_for_core_range_RangeInclusive_Idx.
  
  Module Impl_core_cmp_Eq_where_core_cmp_Eq_Idx_for_core_range_RangeInclusive_Idx.
    Definition Self (Idx : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::range::RangeInclusive") [] [ Idx ].
    
    (* Eq *)
    Definition assert_receiver_is_total_eq
        (Idx : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self Idx in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (Idx : Ty.t),
      M.IsTraitInstance
        "core::cmp::Eq"
        (Self Idx)
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("assert_receiver_is_total_eq", InstanceField.Method (assert_receiver_is_total_eq Idx)) ].
  End Impl_core_cmp_Eq_where_core_cmp_Eq_Idx_for_core_range_RangeInclusive_Idx.
  
  Module Impl_core_hash_Hash_where_core_hash_Hash_Idx_for_core_range_RangeInclusive_Idx.
    Definition Self (Idx : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::range::RangeInclusive") [] [ Idx ].
    
    (* Hash *)
    Definition hash (Idx : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Idx in
      match ε, τ, α with
      | [], [ __H ], [ self; state ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let state := M.alloc (| state |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::hash::Hash", Idx, [], "hash", [ __H ] |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::range::RangeInclusive",
                      "start"
                    |);
                    M.read (| state |)
                  ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (| "core::hash::Hash", Idx, [], "hash", [ __H ] |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::range::RangeInclusive",
                    "end"
                  |);
                  M.read (| state |)
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (Idx : Ty.t),
      M.IsTraitInstance
        "core::hash::Hash"
        (Self Idx)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method (hash Idx)) ].
  End Impl_core_hash_Hash_where_core_hash_Hash_Idx_for_core_range_RangeInclusive_Idx.
  
  Module Impl_core_fmt_Debug_where_core_fmt_Debug_Idx_for_core_range_RangeInclusive_Idx.
    Definition Self (Idx : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::range::RangeInclusive") [] [ Idx ].
    
    (*
        fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
            self.start.fmt(fmt)?;
            write!(fmt, "..=")?;
            self.end.fmt(fmt)?;
            Ok(())
        }
    *)
    Definition fmt (Idx : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Idx in
      match ε, τ, α with
      | [], [], [ self; fmt ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let fmt := M.alloc (| fmt |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::try_trait::Try",
                          Ty.apply
                            (Ty.path "core::result::Result")
                            []
                            [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                          [],
                          "branch",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (| "core::fmt::Debug", Idx, [], "fmt", [] |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::range::RangeInclusive",
                                "start"
                              |);
                              M.read (| fmt |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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::result::Result")
                                        []
                                        [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                                      [
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [
                                            Ty.path "core::convert::Infallible";
                                            Ty.path "core::fmt::Error"
                                          ]
                                      ],
                                      "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))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::try_trait::Try",
                          Ty.apply
                            (Ty.path "core::result::Result")
                            []
                            [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                          [],
                          "branch",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Formatter",
                              "write_fmt",
                              []
                            |),
                            [
                              M.read (| fmt |);
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::Arguments",
                                  "new_const",
                                  []
                                |),
                                [ M.alloc (| Value.Array [ M.read (| Value.String "..=" |) ] |) ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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::result::Result")
                                        []
                                        [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                                      [
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [
                                            Ty.path "core::convert::Infallible";
                                            Ty.path "core::fmt::Error"
                                          ]
                                      ],
                                      "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))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::try_trait::Try",
                          Ty.apply
                            (Ty.path "core::result::Result")
                            []
                            [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                          [],
                          "branch",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (| "core::fmt::Debug", Idx, [], "fmt", [] |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::range::RangeInclusive",
                                "end"
                              |);
                              M.read (| fmt |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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::result::Result")
                                        []
                                        [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                                      [
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [
                                            Ty.path "core::convert::Infallible";
                                            Ty.path "core::fmt::Error"
                                          ]
                                      ],
                                      "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))
                    ]
                  |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (Idx : Ty.t),
      M.IsTraitInstance
        "core::fmt::Debug"
        (Self Idx)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt Idx)) ].
  End Impl_core_fmt_Debug_where_core_fmt_Debug_Idx_for_core_range_RangeInclusive_Idx.
  
  Module Impl_core_range_RangeInclusive_Idx.
    Definition Self (Idx : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::range::RangeInclusive") [] [ Idx ].
    
    (*
        pub fn contains<U>(&self, item: &U) -> bool
        where
            Idx: PartialOrd<U>,
            U: ?Sized + PartialOrd<Idx>,
        {
            <Self as RangeBounds<Idx>>::contains(self, item)
        }
    *)
    Definition contains (Idx : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Idx in
      match ε, τ, α with
      | [], [ U ], [ self; item ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let item := M.alloc (| item |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::ops::range::RangeBounds",
              Ty.apply (Ty.path "core::range::RangeInclusive") [] [ Idx ],
              [ Idx ],
              "contains",
              [ U ]
            |),
            [ M.read (| self |); M.read (| item |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_contains :
      forall (Idx : Ty.t),
      M.IsAssociatedFunction (Self Idx) "contains" (contains Idx).
    
    (*
        pub fn is_empty(&self) -> bool {
            !(self.start <= self.end)
        }
    *)
    Definition is_empty (Idx : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Idx in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          UnOp.not (|
            M.call_closure (|
              M.get_trait_method (| "core::cmp::PartialOrd", Idx, [ Idx ], "le", [] |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::range::RangeInclusive",
                  "start"
                |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::range::RangeInclusive",
                  "end"
                |)
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_empty :
      forall (Idx : Ty.t),
      M.IsAssociatedFunction (Self Idx) "is_empty" (is_empty Idx).
    (*
        pub fn iter(&self) -> IterRangeInclusive<Idx> {
            self.clone().into_iter()
        }
    *)
    Definition iter (Idx : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Idx in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::iter::traits::collect::IntoIterator",
              Ty.apply (Ty.path "core::range::RangeInclusive") [] [ Idx ],
              [],
              "into_iter",
              []
            |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::clone::Clone",
                  Ty.apply (Ty.path "core::range::RangeInclusive") [] [ Idx ],
                  [],
                  "clone",
                  []
                |),
                [ M.read (| self |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_iter :
      forall (Idx : Ty.t),
      M.IsAssociatedFunction (Self Idx) "iter" (iter Idx).
  End Impl_core_range_RangeInclusive_Idx.
  
  
  Module Impl_core_range_RangeInclusive_usize.
    Definition Self : Ty.t :=
      Ty.apply (Ty.path "core::range::RangeInclusive") [] [ Ty.path "usize" ].
    
    (*
        pub(crate) const fn into_slice_range(self) -> Range<usize> {
            Range { start: self.start, end: self.end + 1 }
        }
    *)
    Definition into_slice_range (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructRecord
            "core::range::Range"
            [
              ("start",
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    self,
                    "core::range::RangeInclusive",
                    "start"
                  |)
                |));
              ("end_",
                BinOp.Wrap.add (|
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      self,
                      "core::range::RangeInclusive",
                      "end"
                    |)
                  |),
                  Value.Integer IntegerKind.Usize 1
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_into_slice_range :
      M.IsAssociatedFunction Self "into_slice_range" into_slice_range.
  End Impl_core_range_RangeInclusive_usize.
  
  Module Impl_core_ops_range_RangeBounds_T_for_core_range_RangeInclusive_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::range::RangeInclusive") [] [ T ].
    
    (*
        fn start_bound(&self) -> Bound<&T> {
            Included(&self.start)
        }
    *)
    Definition start_bound (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructTuple
            "core::ops::range::Bound::Included"
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::range::RangeInclusive",
                "start"
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn end_bound(&self) -> Bound<&T> {
            Included(&self.end)
        }
    *)
    Definition end_bound (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructTuple
            "core::ops::range::Bound::Included"
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::range::RangeInclusive",
                "end"
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::ops::range::RangeBounds"
        (Self T)
        (* Trait polymorphic types *) [ (* T *) T ]
        (* Instance *)
        [
          ("start_bound", InstanceField.Method (start_bound T));
          ("end_bound", InstanceField.Method (end_bound T))
        ].
  End Impl_core_ops_range_RangeBounds_T_for_core_range_RangeInclusive_T.
  
  Module Impl_core_ops_range_RangeBounds_T_for_core_range_RangeInclusive_ref__T.
    Definition Self (T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::range::RangeInclusive") [] [ Ty.apply (Ty.path "&") [] [ T ] ].
    
    (*
        fn start_bound(&self) -> Bound<&T> {
            Included(self.start)
        }
    *)
    Definition start_bound (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructTuple
            "core::ops::range::Bound::Included"
            [
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::range::RangeInclusive",
                  "start"
                |)
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn end_bound(&self) -> Bound<&T> {
            Included(self.end)
        }
    *)
    Definition end_bound (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructTuple
            "core::ops::range::Bound::Included"
            [
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::range::RangeInclusive",
                  "end"
                |)
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::ops::range::RangeBounds"
        (Self T)
        (* Trait polymorphic types *) [ (* T *) T ]
        (* Instance *)
        [
          ("start_bound", InstanceField.Method (start_bound T));
          ("end_bound", InstanceField.Method (end_bound T))
        ].
  End Impl_core_ops_range_RangeBounds_T_for_core_range_RangeInclusive_ref__T.
  
  Module Impl_core_convert_From_core_range_RangeInclusive_T_for_core_ops_range_RangeInclusive_T.
    Definition Self (T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ T ].
    
    (*
        fn from(value: RangeInclusive<T>) -> Self {
            Self::new(value.start, value.end)
        }
    *)
    Definition from (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ value ] =>
        ltac:(M.monadic
          (let value := M.alloc (| value |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ T ],
              "new",
              []
            |),
            [
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  value,
                  "core::range::RangeInclusive",
                  "start"
                |)
              |);
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  value,
                  "core::range::RangeInclusive",
                  "end"
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::convert::From"
        (Self T)
        (* Trait polymorphic types *)
        [ (* T *) Ty.apply (Ty.path "core::range::RangeInclusive") [] [ T ] ]
        (* Instance *) [ ("from", InstanceField.Method (from T)) ].
  End Impl_core_convert_From_core_range_RangeInclusive_T_for_core_ops_range_RangeInclusive_T.
  
  Module Impl_core_convert_From_core_ops_range_RangeInclusive_T_for_core_range_RangeInclusive_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::range::RangeInclusive") [] [ T ].
    
    (*
        fn from(value: legacy::RangeInclusive<T>) -> Self {
            assert!(
                !value.exhausted,
                "attempted to convert from an exhausted `legacy::RangeInclusive` (unspecified behavior)"
            );
    
            let (start, end) = value.into_inner();
            RangeInclusive { start, end }
        }
    *)
    Definition from (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ value ] =>
        ltac:(M.monadic
          (let value := M.alloc (| value |) in
          M.read (|
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            UnOp.not (|
                              UnOp.not (|
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    value,
                                    "core::ops::range::RangeInclusive",
                                    "exhausted"
                                  |)
                                |)
                              |)
                            |)
                          |)) 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::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 convert from an exhausted `legacy::RangeInclusive` (unspecified behavior)"
                                        |)
                                      ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ T ],
                    "into_inner",
                    []
                  |),
                  [ M.read (| value |) ]
                |)
              |),
              [
                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.alloc (|
                      Value.StructRecord
                        "core::range::RangeInclusive"
                        [ ("start", M.read (| start |)); ("end_", M.read (| end_ |)) ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::convert::From"
        (Self T)
        (* Trait polymorphic types *)
        [ (* T *) Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ T ] ]
        (* Instance *) [ ("from", InstanceField.Method (from T)) ].
  End Impl_core_convert_From_core_ops_range_RangeInclusive_T_for_core_range_RangeInclusive_T.
  
  (* StructRecord
    {
      name := "RangeFrom";
      const_params := [];
      ty_params := [ "Idx" ];
      fields := [ ("start", Idx) ];
    } *)
  
  Module Impl_core_clone_Clone_where_core_clone_Clone_Idx_for_core_range_RangeFrom_Idx.
    Definition Self (Idx : Ty.t) : Ty.t := Ty.apply (Ty.path "core::range::RangeFrom") [] [ Idx ].
    
    (* Clone *)
    Definition clone (Idx : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Idx in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructRecord
            "core::range::RangeFrom"
            [
              ("start",
                M.call_closure (|
                  M.get_trait_method (| "core::clone::Clone", Idx, [], "clone", [] |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::range::RangeFrom",
                      "start"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (Idx : Ty.t),
      M.IsTraitInstance
        "core::clone::Clone"
        (Self Idx)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method (clone Idx)) ].
  End Impl_core_clone_Clone_where_core_clone_Clone_Idx_for_core_range_RangeFrom_Idx.
  
  Module Impl_core_marker_Copy_where_core_marker_Copy_Idx_for_core_range_RangeFrom_Idx.
    Definition Self (Idx : Ty.t) : Ty.t := Ty.apply (Ty.path "core::range::RangeFrom") [] [ Idx ].
    
    Axiom Implements :
      forall (Idx : Ty.t),
      M.IsTraitInstance
        "core::marker::Copy"
        (Self Idx)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_where_core_marker_Copy_Idx_for_core_range_RangeFrom_Idx.
  
  Module Impl_core_marker_StructuralPartialEq_for_core_range_RangeFrom_Idx.
    Definition Self (Idx : Ty.t) : Ty.t := Ty.apply (Ty.path "core::range::RangeFrom") [] [ Idx ].
    
    Axiom Implements :
      forall (Idx : Ty.t),
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        (Self Idx)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_core_range_RangeFrom_Idx.
  
  Module Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_Idx_for_core_range_RangeFrom_Idx.
    Definition Self (Idx : Ty.t) : Ty.t := Ty.apply (Ty.path "core::range::RangeFrom") [] [ Idx ].
    
    (* PartialEq *)
    Definition eq (Idx : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Idx in
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_trait_method (| "core::cmp::PartialEq", Idx, [ Idx ], "eq", [] |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::range::RangeFrom",
                "start"
              |);
              M.SubPointer.get_struct_record_field (|
                M.read (| other |),
                "core::range::RangeFrom",
                "start"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (Idx : Ty.t),
      M.IsTraitInstance
        "core::cmp::PartialEq"
        (Self Idx)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method (eq Idx)) ].
  End Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_Idx_for_core_range_RangeFrom_Idx.
  
  Module Impl_core_cmp_Eq_where_core_cmp_Eq_Idx_for_core_range_RangeFrom_Idx.
    Definition Self (Idx : Ty.t) : Ty.t := Ty.apply (Ty.path "core::range::RangeFrom") [] [ Idx ].
    
    (* Eq *)
    Definition assert_receiver_is_total_eq
        (Idx : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self Idx in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (Idx : Ty.t),
      M.IsTraitInstance
        "core::cmp::Eq"
        (Self Idx)
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("assert_receiver_is_total_eq", InstanceField.Method (assert_receiver_is_total_eq Idx)) ].
  End Impl_core_cmp_Eq_where_core_cmp_Eq_Idx_for_core_range_RangeFrom_Idx.
  
  Module Impl_core_hash_Hash_where_core_hash_Hash_Idx_for_core_range_RangeFrom_Idx.
    Definition Self (Idx : Ty.t) : Ty.t := Ty.apply (Ty.path "core::range::RangeFrom") [] [ Idx ].
    
    (* Hash *)
    Definition hash (Idx : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Idx in
      match ε, τ, α with
      | [], [ __H ], [ self; state ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let state := M.alloc (| state |) in
          M.call_closure (|
            M.get_trait_method (| "core::hash::Hash", Idx, [], "hash", [ __H ] |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::range::RangeFrom",
                "start"
              |);
              M.read (| state |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (Idx : Ty.t),
      M.IsTraitInstance
        "core::hash::Hash"
        (Self Idx)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method (hash Idx)) ].
  End Impl_core_hash_Hash_where_core_hash_Hash_Idx_for_core_range_RangeFrom_Idx.
  
  Module Impl_core_fmt_Debug_where_core_fmt_Debug_Idx_for_core_range_RangeFrom_Idx.
    Definition Self (Idx : Ty.t) : Ty.t := Ty.apply (Ty.path "core::range::RangeFrom") [] [ Idx ].
    
    (*
        fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
            self.start.fmt(fmt)?;
            write!(fmt, "..")?;
            Ok(())
        }
    *)
    Definition fmt (Idx : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Idx in
      match ε, τ, α with
      | [], [], [ self; fmt ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let fmt := M.alloc (| fmt |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::try_trait::Try",
                          Ty.apply
                            (Ty.path "core::result::Result")
                            []
                            [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                          [],
                          "branch",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (| "core::fmt::Debug", Idx, [], "fmt", [] |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::range::RangeFrom",
                                "start"
                              |);
                              M.read (| fmt |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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::result::Result")
                                        []
                                        [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                                      [
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [
                                            Ty.path "core::convert::Infallible";
                                            Ty.path "core::fmt::Error"
                                          ]
                                      ],
                                      "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))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::try_trait::Try",
                          Ty.apply
                            (Ty.path "core::result::Result")
                            []
                            [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                          [],
                          "branch",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Formatter",
                              "write_fmt",
                              []
                            |),
                            [
                              M.read (| fmt |);
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::Arguments",
                                  "new_const",
                                  []
                                |),
                                [ M.alloc (| Value.Array [ M.read (| Value.String ".." |) ] |) ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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::result::Result")
                                        []
                                        [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                                      [
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [
                                            Ty.path "core::convert::Infallible";
                                            Ty.path "core::fmt::Error"
                                          ]
                                      ],
                                      "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))
                    ]
                  |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (Idx : Ty.t),
      M.IsTraitInstance
        "core::fmt::Debug"
        (Self Idx)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt Idx)) ].
  End Impl_core_fmt_Debug_where_core_fmt_Debug_Idx_for_core_range_RangeFrom_Idx.
  
  Module Impl_core_range_RangeFrom_Idx.
    Definition Self (Idx : Ty.t) : Ty.t := Ty.apply (Ty.path "core::range::RangeFrom") [] [ Idx ].
    
    (*
        pub fn iter(&self) -> IterRangeFrom<Idx> {
            self.clone().into_iter()
        }
    *)
    Definition iter (Idx : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Idx in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::iter::traits::collect::IntoIterator",
              Ty.apply (Ty.path "core::range::RangeFrom") [] [ Idx ],
              [],
              "into_iter",
              []
            |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::clone::Clone",
                  Ty.apply (Ty.path "core::range::RangeFrom") [] [ Idx ],
                  [],
                  "clone",
                  []
                |),
                [ M.read (| self |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_iter :
      forall (Idx : Ty.t),
      M.IsAssociatedFunction (Self Idx) "iter" (iter Idx).
    (*
        pub fn contains<U>(&self, item: &U) -> bool
        where
            Idx: PartialOrd<U>,
            U: ?Sized + PartialOrd<Idx>,
        {
            <Self as RangeBounds<Idx>>::contains(self, item)
        }
    *)
    Definition contains (Idx : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Idx in
      match ε, τ, α with
      | [], [ U ], [ self; item ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let item := M.alloc (| item |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::ops::range::RangeBounds",
              Ty.apply (Ty.path "core::range::RangeFrom") [] [ Idx ],
              [ Idx ],
              "contains",
              [ U ]
            |),
            [ M.read (| self |); M.read (| item |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_contains :
      forall (Idx : Ty.t),
      M.IsAssociatedFunction (Self Idx) "contains" (contains Idx).
  End Impl_core_range_RangeFrom_Idx.
  
  
  Module Impl_core_ops_range_RangeBounds_T_for_core_range_RangeFrom_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::range::RangeFrom") [] [ T ].
    
    (*
        fn start_bound(&self) -> Bound<&T> {
            Included(&self.start)
        }
    *)
    Definition start_bound (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructTuple
            "core::ops::range::Bound::Included"
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::range::RangeFrom",
                "start"
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn end_bound(&self) -> Bound<&T> {
            Unbounded
        }
    *)
    Definition end_bound (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructTuple "core::ops::range::Bound::Unbounded" []))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::ops::range::RangeBounds"
        (Self T)
        (* Trait polymorphic types *) [ (* T *) T ]
        (* Instance *)
        [
          ("start_bound", InstanceField.Method (start_bound T));
          ("end_bound", InstanceField.Method (end_bound T))
        ].
  End Impl_core_ops_range_RangeBounds_T_for_core_range_RangeFrom_T.
  
  Module Impl_core_ops_range_RangeBounds_T_for_core_range_RangeFrom_ref__T.
    Definition Self (T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::range::RangeFrom") [] [ Ty.apply (Ty.path "&") [] [ T ] ].
    
    (*
        fn start_bound(&self) -> Bound<&T> {
            Included(self.start)
        }
    *)
    Definition start_bound (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructTuple
            "core::ops::range::Bound::Included"
            [
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::range::RangeFrom",
                  "start"
                |)
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn end_bound(&self) -> Bound<&T> {
            Unbounded
        }
    *)
    Definition end_bound (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructTuple "core::ops::range::Bound::Unbounded" []))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::ops::range::RangeBounds"
        (Self T)
        (* Trait polymorphic types *) [ (* T *) T ]
        (* Instance *)
        [
          ("start_bound", InstanceField.Method (start_bound T));
          ("end_bound", InstanceField.Method (end_bound T))
        ].
  End Impl_core_ops_range_RangeBounds_T_for_core_range_RangeFrom_ref__T.
  
  Module Impl_core_convert_From_core_range_RangeFrom_T_for_core_ops_range_RangeFrom_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ T ].
    
    (*
        fn from(value: RangeFrom<T>) -> Self {
            Self { start: value.start }
        }
    *)
    Definition from (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ value ] =>
        ltac:(M.monadic
          (let value := M.alloc (| value |) in
          Value.StructRecord
            "core::ops::range::RangeFrom"
            [
              ("start",
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    value,
                    "core::range::RangeFrom",
                    "start"
                  |)
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::convert::From"
        (Self T)
        (* Trait polymorphic types *)
        [ (* T *) Ty.apply (Ty.path "core::range::RangeFrom") [] [ T ] ]
        (* Instance *) [ ("from", InstanceField.Method (from T)) ].
  End Impl_core_convert_From_core_range_RangeFrom_T_for_core_ops_range_RangeFrom_T.
  
  Module Impl_core_convert_From_core_ops_range_RangeFrom_T_for_core_range_RangeFrom_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::range::RangeFrom") [] [ T ].
    
    (*
        fn from(value: legacy::RangeFrom<T>) -> Self {
            Self { start: value.start }
        }
    *)
    Definition from (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ value ] =>
        ltac:(M.monadic
          (let value := M.alloc (| value |) in
          Value.StructRecord
            "core::range::RangeFrom"
            [
              ("start",
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    value,
                    "core::ops::range::RangeFrom",
                    "start"
                  |)
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::convert::From"
        (Self T)
        (* Trait polymorphic types *)
        [ (* T *) Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ T ] ]
        (* Instance *) [ ("from", InstanceField.Method (from T)) ].
  End Impl_core_convert_From_core_ops_range_RangeFrom_T_for_core_range_RangeFrom_T.
End range.
