case h.h
α : Type u_1
L : List (List α)
⊢ sections L = sectionsTR L
⊢ @sections = @sectionsTR
funext α L
case h.h
α : Type u_1
L : List (List α)
⊢ sections L = bif any L isEmpty then [] else (foldr sectionsTR.go #[[]] L).data
case h.h
α : Type u_1
L : List (List α)
⊢ sections L = sectionsTR L
simp [sectionsTR]
case h.h.false
α : Type u_1
L : List (List α)
e : any L isEmpty = false
⊢ sections L = (foldr sectionsTR.go #[[]] L).data
case h.h
α : Type u_1
L : List (List α)
⊢ sections L = bif any L isEmpty then [] else (foldr sectionsTR.go #[[]] L).data
cases e : L.any isEmpty <;> simp [sections_eq_nil_of_isEmpty, *]
case h.h.false
α : Type u_1
L : List (List α)
⊢ sections L = (foldr sectionsTR.go #[[]] L).data
case h.h.false
α : Type u_1
L : List (List α)
e : any L isEmpty = false
⊢ sections L = (foldr sectionsTR.go #[[]] L).data
clear e
case h.h.false.cons
α : Type u_1
l : List α
L : List (List α)
IH : sections L = (foldr sectionsTR.go #[[]] L).data
⊢ sections (l :: L) = (foldr sectionsTR.go #[[]] (l :: L)).data
case h.h.false
α : Type u_1
L : List (List α)
⊢ sections L = (foldr sectionsTR.go #[[]] L).data
induction L with | nil => rfl | cons l L IH => ?_
case h.h.false.cons
α : Type u_1
l : List α
L : List (List α)
IH : sections L = (foldr sectionsTR.go #[[]] L).data
⊢ (List.bind
      (foldr (fun l acc => foldl (fun acc' l' => foldl (fun acc' a => Array.push acc' (a :: l')) acc' l) #[] acc.data)
          #[[]] L).data
      fun s => map (fun a => a :: s) l) =
    (foldl (fun acc' l' => foldl (fun acc' a => Array.push acc' (a :: l')) acc' l) #[]
        (foldr (fun l acc => foldl (fun acc' l' => foldl (fun acc' a => Array.push acc' (a :: l')) acc' l) #[] acc.data)
            #[[]] L).data).data
case h.h.false.cons
α : Type u_1
l : List α
L : List (List α)
IH : sections L = (foldr sectionsTR.go #[[]] L).data
⊢ sections (l :: L) = (foldr sectionsTR.go #[[]] (l :: L)).data
simp [IH, sectionsTR.go, Array.foldl_eq_foldl_data]
case h.h.false.cons
α : Type u_1
l : List α
L : List (List α)
IH : sections L = (foldr sectionsTR.go #[[]] L).data
⊢ (List.bind
      (foldr (fun l acc => foldl (fun acc' l' => foldl (fun acc' a => Array.push acc' (a :: l')) acc' l) #[] acc.data)
          #[[]] L).data
      fun s => map (fun a => a :: s) l) =
    #[].data ++
      List.bind
        (foldr (fun l acc => foldl (fun acc' l' => foldl (fun acc' a => Array.push acc' (a :: l')) acc' l) #[] acc.data)
            #[[]] L).data
        ?h.h.false.cons.G

case h.h.false.cons.G
α : Type u_1
l : List α
L : List (List α)
IH : sections L = (foldr sectionsTR.go #[[]] L).data
⊢ List α → List (List α)

case h.h.false.cons.H
α : Type u_1
l : List α
L : List (List α)
IH : sections L = (foldr sectionsTR.go #[[]] L).data
⊢ ∀ (acc : Array (List α)) (a : List α),
    (foldl (fun acc' a_1 => Array.push acc' (a_1 :: a)) acc l).data = acc.data ++ ?h.h.false.cons.G a
case h.h.false.cons
α : Type u_1
l : List α
L : List (List α)
IH : sections L = (foldr sectionsTR.go #[[]] L).data
⊢ (List.bind
      (foldr (fun l acc => foldl (fun acc' l' => foldl (fun acc' a => Array.push acc' (a :: l')) acc' l) #[] acc.data)
          #[[]] L).data
      fun s => map (fun a => a :: s) l) =
    (foldl (fun acc' l' => foldl (fun acc' a => Array.push acc' (a :: l')) acc' l) #[]
        (foldr (fun l acc => foldl (fun acc' l' => foldl (fun acc' a => Array.push acc' (a :: l')) acc' l) #[] acc.data)
            #[[]] L).data).data
rw [Array.foldl_data_eq_bind]
case h.h.false.cons.H
α : Type u_1
l : List α
L : List (List α)
IH : sections L = (foldr sectionsTR.go #[[]] L).data
⊢ ∀ (acc : Array (List α)) (a : List α),
    (foldl (fun acc' a_1 => Array.push acc' (a_1 :: a)) acc l).data = acc.data ++ map (fun a_1 => a_1 :: a) l
case h.h.false.cons
α : Type u_1
l : List α
L : List (List α)
IH : sections L = (foldr sectionsTR.go #[[]] L).data
⊢ (List.bind
      (foldr (fun l acc => foldl (fun acc' l' => foldl (fun acc' a => Array.push acc' (a :: l')) acc' l) #[] acc.data)
          #[[]] L).data
      fun s => map (fun a => a :: s) l) =
    #[].data ++
      List.bind
        (foldr (fun l acc => foldl (fun acc' l' => foldl (fun acc' a => Array.push acc' (a :: l')) acc' l) #[] acc.data)
            #[[]] L).data
        ?h.h.false.cons.G

case h.h.false.cons.G
α : Type u_1
l : List α
L : List (List α)
IH : sections L = (foldr sectionsTR.go #[[]] L).data
⊢ List α → List (List α)

case h.h.false.cons.H
α : Type u_1
l : List α
L : List (List α)
IH : sections L = (foldr sectionsTR.go #[[]] L).data
⊢ ∀ (acc : Array (List α)) (a : List α),
    (foldl (fun acc' a_1 => Array.push acc' (a_1 :: a)) acc l).data = acc.data ++ ?h.h.false.cons.G a
rfl
case h.h.false.cons.H
α : Type u_1
l : List α
L : List (List α)
IH : sections L = (foldr sectionsTR.go #[[]] L).data
acc✝ : Array (List α)
a✝ : List α
⊢ (foldl (fun acc' a => Array.push acc' (a :: a✝)) acc✝ l).data = acc✝.data ++ map (fun a => a :: a✝) l
case h.h.false.cons.H
α : Type u_1
l : List α
L : List (List α)
IH : sections L = (foldr sectionsTR.go #[[]] L).data
⊢ ∀ (acc : Array (List α)) (a : List α),
    (foldl (fun acc' a_1 => Array.push acc' (a_1 :: a)) acc l).data = acc.data ++ map (fun a_1 => a_1 :: a) l
intros
no goals
case h.h.false.cons.H
α : Type u_1
l : List α
L : List (List α)
IH : sections L = (foldr sectionsTR.go #[[]] L).data
acc✝ : Array (List α)
a✝ : List α
⊢ (foldl (fun acc' a => Array.push acc' (a :: a✝)) acc✝ l).data = acc✝.data ++ map (fun a => a :: a✝) l
apply Array.foldl_data_eq_map
no goals
case h.h.false.nil
α : Type u_1
⊢ sections [] = (foldr sectionsTR.go #[[]] []).data
rfl