theorem LaPToP.DataStructures.Str.append_nil.{u}
  {α : Type u}
  (S : LaPToP.DataStructures.Str α) :
  S ++ LaPToP.DataStructures.Str.nil = S

theorem LaPToP.DataStructures.Str.append_nil.{u}
  {α : Type u}
  (S : LaPToP.DataStructures.Str α) :
  S ++ LaPToP.DataStructures.Str.nil = S

theorem LaPToP.DataStructures.Str.nil_append.{u}
  {α : Type u}
  (S : LaPToP.DataStructures.Str α) :
  LaPToP.DataStructures.Str.nil ++ S = S

theorem LaPToP.DataStructures.Str.append_assoc.{u}
  {α : Type u}
  (S T U : LaPToP.DataStructures.Str α) :
  S ++ (T ++ U) = S ++ T ++ U

theorem LaPToP.DataStructures.Str.len_nil.{u}
  {α : Type u} :
  LaPToP.DataStructures.Str.nil.len = 0

theorem LaPToP.DataStructures.Str.len_item.{u}
  {α : Type u} (i : α) :
  (LaPToP.DataStructures.Str.item i).len =
    1

theorem LaPToP.DataStructures.Str.len_append.{u}
  {α : Type u}
  (S T : LaPToP.DataStructures.Str α) :
  (S ++ T).len = S.len + T.len

theorem LaPToP.DataStructures.Str.append_item_append_inj.{u}
  {α : Type u}
  (S T : LaPToP.DataStructures.Str α)
  (i j : α) :
  i = j ↔
    S ++
          LaPToP.DataStructures.Str.item
            i ++
        T =
      S ++
          LaPToP.DataStructures.Str.item
            j ++
        T

theorem LaPToP.DataStructures.Str.sub_nil.{u}
  {α : Type u} [Inhabited α]
  (S : LaPToP.DataStructures.Str α) :
  S.sub LaPToP.DataStructures.Str.nil =
    LaPToP.DataStructures.Str.nil

theorem LaPToP.DataStructures.Str.at_append_item_append.{u}
  {α : Type u} [Inhabited α]
  (S T : LaPToP.DataStructures.Str α)
  (i : α) :
  (S ++
            LaPToP.DataStructures.Str.item
              i ++
          T).at
      (List.length S) =
    i

theorem LaPToP.DataStructures.Str.sub_append.{u}
  {α : Type u} [Inhabited α]
  (S : LaPToP.DataStructures.Str α)
  (T U : LaPToP.DataStructures.Str ℕ) :
  S.sub (T ++ U) = S.sub T ++ S.sub U

theorem LaPToP.DataStructures.Str.sub_sub.{u}
  {α : Type u} [Inhabited α]
  (S : LaPToP.DataStructures.Str α)
  (T U : LaPToP.DataStructures.Str ℕ)
  (hU : ∀ k ∈ U, k < List.length T) :
  S.sub (T.sub U) = (S.sub T).sub U

theorem LaPToP.DataStructures.Str.at_map_of_lt.{u,
    v}
  {α : Type u} [Inhabited α] {β : Type v}
  [Inhabited β] (f : α → β)
  (T : LaPToP.DataStructures.Str α)
  {k : ℕ} (hk : k < List.length T) :
  LaPToP.DataStructures.Str.at
      (List.map f T) k =
    f (T.at k)

theorem LaPToP.DataStructures.Str.copies_zero.{u}
  {α : Type u}
  (S : LaPToP.DataStructures.Str α) :
  LaPToP.DataStructures.Str.copies 0 S =
    LaPToP.DataStructures.Str.nil

theorem LaPToP.DataStructures.Str.copies_succ.{u}
  {α : Type u}
  (S : LaPToP.DataStructures.Str α)
  (n : ℕ) :
  LaPToP.DataStructures.Str.copies (n + 1)
      S =
    LaPToP.DataStructures.Str.copies n
        S ++
      S

theorem LaPToP.DataStructures.Str.copies_three_example :
  LaPToP.DataStructures.Str.copies 3
      [0, 1] =
    [0, 1, 0, 1, 0, 1]

theorem LaPToP.DataStructures.Str.mem_star.{u}
  {α : Type u}
  (S T : LaPToP.DataStructures.Str α) :
  T ∈ S.star ↔
    ∃ n,
      LaPToP.DataStructures.Str.copies n
          S =
        T

theorem LaPToP.DataStructures.Str.update_append_item_append.{u}
  {α : Type u}
  (S T : LaPToP.DataStructures.Str α)
  (i j : α) :
  (S ++
            LaPToP.DataStructures.Str.item
              i ++
          T).update
      (List.length S) j =
    S ++
        LaPToP.DataStructures.Str.item
          j ++
      T

theorem LaPToP.DataStructures.Str.update_example :
  LaPToP.DataStructures.Str.update
      [3, 5, 9] 2 8 =
    [3, 5, 8]

theorem LaPToP.DataStructures.Str.nil_le.{u}
  {α : Type u} [LT α]
  (S : LaPToP.DataStructures.Str α) :
  LaPToP.DataStructures.Str.nil ≤ S

theorem LaPToP.DataStructures.Str.lt_append_item_append.{u}
  {α : Type u} [LT α]
  (S T : LaPToP.DataStructures.Str α)
  (i : α) :
  S <
    S ++
        LaPToP.DataStructures.Str.item
          i ++
      T

theorem LaPToP.DataStructures.Str.append_lt_append_of_lt.{u}
  {α : Type u} [LT α]
  (S T U : LaPToP.DataStructures.Str α)
  (i j : α) (h : i < j) :
  S ++ LaPToP.DataStructures.Str.item i ++
      T <
    S ++
        LaPToP.DataStructures.Str.item
          j ++
      U

theorem LaPToP.DataStructures.Str.len_interval
  (x y : ℤ) :
  (LaPToP.DataStructures.Str.interval x
        y).len =
    ↑(y - x).toNat

theorem LaPToP.DataStructures.Str.interval_self
  (x : ℤ) :
  LaPToP.DataStructures.Str.interval x x =
    LaPToP.DataStructures.Str.nil

theorem LaPToP.DataStructures.Str.interval_succ
  (x : ℤ) :
  LaPToP.DataStructures.Str.interval x
      (x + 1) =
    LaPToP.DataStructures.Str.item x

theorem LaPToP.DataStructures.Str.interval_append_interval
  {x y z : ℤ} (hxy : x ≤ y)
  (hyz : y ≤ z) :
  LaPToP.DataStructures.Str.interval x
        y ++
      LaPToP.DataStructures.Str.interval y
        z =
    LaPToP.DataStructures.Str.interval x z

theorem LaPToP.DataStructures.Str.mem_interval
  (i x y : ℤ) :
  i ∈
      LaPToP.DataStructures.Str.interval x
        y ↔
    x ≤ i ∧ i < y

theorem LaPToP.DataStructures.HList.pack_contents.{u}
  {α : Type u}
  (L : LaPToP.DataStructures.HList α) :
  L.contents.pack = L

theorem LaPToP.DataStructures.HList.contents_pack.{u}
  {α : Type u}
  (S : LaPToP.DataStructures.Str α) :
  S.pack.contents = S

theorem LaPToP.DataStructures.HList.length_pack.{u}
  {α : Type u}
  (S : LaPToP.DataStructures.Str α) :
  S.pack.length = S.len

theorem LaPToP.DataStructures.HList.domain_eq.{u}
  {α : Type u}
  (L : LaPToP.DataStructures.HList α) :
  L.domain =
    {n | n < List.length L.contents}

theorem LaPToP.DataStructures.HList.image_domain.{u}
  {α : Type u}
  (L : LaPToP.DataStructures.HList α) :
  Nat.cast '' L.domain =
    LaPToP.BasicTheories.Bunch.interval 0
      ↑(List.length L.contents)

theorem LaPToP.DataStructures.HList.pack_join_pack.{u}
  {α : Type u}
  (S T : LaPToP.DataStructures.Str α) :
  S.pack.join T.pack = (S ++ T).pack

theorem LaPToP.DataStructures.HList.at_pack.{u}
  {α : Type u}
  (S : LaPToP.DataStructures.Str α)
  (n : ℕ) [Inhabited α] :
  S.pack.at n = S.at n

theorem LaPToP.DataStructures.HList.pack_comp_pack.{u}
  {α : Type u}
  (S : LaPToP.DataStructures.Str α)
  [Inhabited α]
  (T : LaPToP.DataStructures.Str ℕ) :
  S.pack.comp T.pack = (S.sub T).pack

theorem LaPToP.DataStructures.HList.modify_pack.{u}
  {α : Type u}
  (S : LaPToP.DataStructures.Str α)
  (n : ℕ) (i : α) :
  LaPToP.DataStructures.HList.modify n i
      S.pack =
    (S.update n i).pack

theorem LaPToP.DataStructures.HList.pack_inj.{u}
  {α : Type u}
  (S T : LaPToP.DataStructures.Str α) :
  S.pack = T.pack ↔ S = T

theorem LaPToP.DataStructures.HList.pack_lt_pack.{u}
  {α : Type u}
  (S T : LaPToP.DataStructures.Str α)
  [LT α] : S.pack < T.pack ↔ S < T

theorem LaPToP.DataStructures.HList.image_pack_subset_image_pack.{u}
  {α : Type u}
  (A B :
    LaPToP.BasicTheories.Bunch
      (LaPToP.DataStructures.Str α)) :
  LaPToP.DataStructures.Str.pack '' A ⊆
      LaPToP.DataStructures.Str.pack ''
        B ↔
    A ⊆ B

theorem LaPToP.DataStructures.Str.pack_injective.{u}
  {α : Type u} :
  Function.Injective
    LaPToP.DataStructures.Str.pack

theorem LaPToP.DataStructures.HList.contents_example :
  (LaPToP.DataStructures.Str.pack
        [3, 5, 7, 4]).contents =
    [3, 5, 7, 4]

theorem LaPToP.DataStructures.HList.length_example :
  (LaPToP.DataStructures.Str.pack
        [3, 5, 7, 4]).length =
    4

theorem LaPToP.DataStructures.HList.at_example :
  (LaPToP.DataStructures.Str.pack
          [3, 5, 7, 4]).at
      2 =
    7

theorem LaPToP.DataStructures.HList.comp_example :
  (LaPToP.DataStructures.Str.pack
          [3, 5, 7, 4]).comp
      (LaPToP.DataStructures.Str.pack
        [2, 1, 2]) =
    LaPToP.DataStructures.Str.pack
      [7, 5, 7]

theorem LaPToP.DataStructures.HList.join_example :
  (LaPToP.DataStructures.Str.pack
          [3, 5, 7, 4]).join
      (LaPToP.DataStructures.Str.pack
        [2, 1, 2]) =
    LaPToP.DataStructures.Str.pack
      [3, 5, 7, 4, 2, 1, 2]

theorem LaPToP.DataStructures.HList.modify_example :
  LaPToP.DataStructures.HList.modify 2 22
      (LaPToP.DataStructures.Str.interval
          10 15).pack =
    LaPToP.DataStructures.Str.pack
      [10, 11, 22, 13, 14]

theorem LaPToP.DataStructures.HList.modify_modify_example :
  LaPToP.DataStructures.HList.modify 2 22
      (LaPToP.DataStructures.HList.modify
        3 33
        (LaPToP.DataStructures.Str.interval
            10 15).pack) =
    LaPToP.DataStructures.Str.pack
      [10, 11, 22, 33, 14]

theorem LaPToP.DataStructures.HList.modify_swap_example :
  have L :=
    (LaPToP.DataStructures.Str.interval 10
        15).pack;
  LaPToP.DataStructures.HList.modify 2
      (L.at 3)
      (LaPToP.DataStructures.HList.modify
        3 (L.at 2) L) =
    LaPToP.DataStructures.Str.pack
      [10, 11, 13, 12, 14]