α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ tail (initsCore [head s] (tail s)) = initsCore [head s, head (tail s)] (tail (tail s))
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ tail (inits s) = initsCore [head s, head (tail s)] (tail (tail s))
unfold inits
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ tail ([head s] :: initsCore ([head s] ++ [head (tail s)]) (tail (tail s))) =
    initsCore [head s, head (tail s)] (tail (tail s))
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ tail (initsCore [head s] (tail s)) = initsCore [head s, head (tail s)] (tail (tail s))
rw [inits_core_eq]
no goals
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ tail ([head s] :: initsCore ([head s] ++ [head (tail s)]) (tail (tail s))) =
    initsCore [head s, head (tail s)] (tail (tail s))
rfl