case h.h
α : Type u
β : Type v
γ : Type w
a : α
r : List (List α)
⊢ sublistsAux a r =
    Array.toList
      (Array.foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r) 0 (Array.size (toArray r)))
α : Type u
β : Type v
γ : Type w
⊢ sublistsAux = fun a r =>
    Array.toList
      (Array.foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r) 0 (Array.size (toArray r)))
funext a r
case h.h
α : Type u
β : Type v
γ : Type w
a : α
r : List (List α)
⊢ foldl (fun r l => r ++ [l, a :: l]) [] r =
    Array.toList (foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r).data)
case h.h
α : Type u
β : Type v
γ : Type w
a : α
r : List (List α)
⊢ sublistsAux a r =
    Array.toList
      (Array.foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r) 0 (Array.size (toArray r)))
simp only [sublistsAux, Array.foldl_eq_foldl_data, Array.mkEmpty]
case h.h
α : Type u
β : Type v
γ : Type w
a : α
r : List (List α)
this :
  foldl (fun r l => r ++ [l, a :: l]) (Array.toList #[]) r =
    Array.toList (foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] r)
⊢ foldl (fun r l => r ++ [l, a :: l]) [] r =
    Array.toList (foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r).data)
case h.h
α : Type u
β : Type v
γ : Type w
a : α
r : List (List α)
⊢ foldl (fun r l => r ++ [l, a :: l]) [] r =
    Array.toList (foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r).data)
have := foldl_hom Array.toList (fun r l => (r.push l).push (a :: l))
  (fun (r : List (List α)) l => r ++ [l, a :: l]) r #[]
  (by simp)
no goals
case h.h
α : Type u
β : Type v
γ : Type w
a : α
r : List (List α)
this :
  foldl (fun r l => r ++ [l, a :: l]) (Array.toList #[]) r =
    Array.toList (foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] r)
⊢ foldl (fun r l => r ++ [l, a :: l]) [] r =
    Array.toList (foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r).data)
simpa using this
no goals
α : Type u
β : Type v
γ : Type w
a : α
r : List (List α)
⊢ ∀ (x : Array (List α)) (y : List α),
    (fun r l => r ++ [l, a :: l]) (Array.toList x) y =
      Array.toList ((fun r l => Array.push (Array.push r l) (a :: l)) x y)
simp