α : Type u
β : Type v
γ : Type w
l : List α
⊢ Array.toList
      (foldr (fun a arr => Array.foldl (fun r l => Array.push r (a :: l)) arr arr 0 (Array.size arr)) #[[]] l) =
    foldr
      (fun a r =>
        Array.toList
          (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r) (toArray r) 0 (Array.size (toArray r))))
      [[]] l
α : Type u
β : Type v
γ : Type w
l : List α
⊢ sublists' l = foldr (fun a r => sublists'Aux a r r) [[]] l
simp only [sublists', sublists'Aux_eq_array_foldl]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ Array.toList
      (foldr (fun a arr => Array.foldl (fun r l => Array.push r (a :: l)) arr arr 0 (Array.size arr)) #[[]] l) =
    foldr
      (fun a r =>
        Array.toList
          (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r) (toArray r) 0 (Array.size (toArray r))))
      [[]] l
α : Type u
β : Type v
γ : Type w
l : List α
⊢ Array.toList
      (foldr (fun a arr => Array.foldl (fun r l => Array.push r (a :: l)) arr arr 0 (Array.size arr)) #[[]] l) =
    foldr
      (fun a r =>
        Array.toList
          (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r) (toArray r) 0 (Array.size (toArray r))))
      [[]] l
dsimp only
α : Type u
β : Type v
γ : Type w
l : List α
⊢ foldr ?g₂ (Array.toList #[[]]) l =
    foldr
      (fun a r =>
        Array.toList
          (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r) (toArray r) 0 (Array.size (toArray r))))
      [[]] l

case g₂
α : Type u
β : Type v
γ : Type w
l : List α
⊢ α → List (List α) → List (List α)

case H
α : Type u
β : Type v
γ : Type w
l : List α
⊢ ∀ (x : α) (y : Array (List α)),
    ?g₂ x (Array.toList y) = Array.toList (Array.foldl (fun r l => Array.push r (x :: l)) y y 0 (Array.size y))
α : Type u
β : Type v
γ : Type w
l : List α
⊢ Array.toList
      (foldr (fun a arr => Array.foldl (fun r l => Array.push r (a :: l)) arr arr 0 (Array.size arr)) #[[]] l) =
    foldr
      (fun a r =>
        Array.toList
          (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r) (toArray r) 0 (Array.size (toArray r))))
      [[]] l
rw [← List.foldr_hom Array.toList]
case H
α : Type u
β : Type v
γ : Type w
l : List α
⊢ ∀ (x : α) (y : Array (List α)),
    Array.toList
        (Array.foldl (fun r l => Array.push r (x :: l)) (toArray (Array.toList y)) (toArray (Array.toList y)) 0
          (Array.size (toArray (Array.toList y)))) =
      Array.toList (Array.foldl (fun r l => Array.push r (x :: l)) y y 0 (Array.size y))
α : Type u
β : Type v
γ : Type w
l : List α
⊢ foldr ?g₂ (Array.toList #[[]]) l =
    foldr
      (fun a r =>
        Array.toList
          (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r) (toArray r) 0 (Array.size (toArray r))))
      [[]] l

case g₂
α : Type u
β : Type v
γ : Type w
l : List α
⊢ α → List (List α) → List (List α)

case H
α : Type u
β : Type v
γ : Type w
l : List α
⊢ ∀ (x : α) (y : Array (List α)),
    ?g₂ x (Array.toList y) = Array.toList (Array.foldl (fun r l => Array.push r (x :: l)) y y 0 (Array.size y))
. rfl
no goals
case H
α : Type u
β : Type v
γ : Type w
l : List α
⊢ ∀ (x : α) (y : Array (List α)),
    Array.toList
        (Array.foldl (fun r l => Array.push r (x :: l)) (toArray (Array.toList y)) (toArray (Array.toList y)) 0
          (Array.size (toArray (Array.toList y)))) =
      Array.toList (Array.foldl (fun r l => Array.push r (x :: l)) y y 0 (Array.size y))
. intros _ _; congr <;> simp
no goals
α : Type u
β : Type v
γ : Type w
l : List α
⊢ foldr ?g₂ (Array.toList #[[]]) l =
    foldr
      (fun a r =>
        Array.toList
          (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r) (toArray r) 0 (Array.size (toArray r))))
      [[]] l
rfl
case H
α : Type u
β : Type v
γ : Type w
l : List α
x✝ : α
y✝ : Array (List α)
⊢ Array.toList
      (Array.foldl (fun r l => Array.push r (x✝ :: l)) (toArray (Array.toList y✝)) (toArray (Array.toList y✝)) 0
        (Array.size (toArray (Array.toList y✝)))) =
    Array.toList (Array.foldl (fun r l => Array.push r (x✝ :: l)) y✝ y✝ 0 (Array.size y✝))
case H
α : Type u
β : Type v
γ : Type w
l : List α
⊢ ∀ (x : α) (y : Array (List α)),
    Array.toList
        (Array.foldl (fun r l => Array.push r (x :: l)) (toArray (Array.toList y)) (toArray (Array.toList y)) 0
          (Array.size (toArray (Array.toList y)))) =
      Array.toList (Array.foldl (fun r l => Array.push r (x :: l)) y y 0 (Array.size y))
intros _ _
no goals
case H
α : Type u
β : Type v
γ : Type w
l : List α
x✝ : α
y✝ : Array (List α)
⊢ Array.toList
      (Array.foldl (fun r l => Array.push r (x✝ :: l)) (toArray (Array.toList y✝)) (toArray (Array.toList y✝)) 0
        (Array.size (toArray (Array.toList y✝)))) =
    Array.toList (Array.foldl (fun r l => Array.push r (x✝ :: l)) y✝ y✝ 0 (Array.size y✝))
congr <;> simp