α : Type u
β : Type v
δ : Type w
l : List α
s : Stream' α
⊢ corec
      (fun x =>
        match x with
        | (a, snd) => a)
      (fun p =>
        match p with
        | (l', s') => (l' ++ [head s'], tail s'))
      (l, s) =
    l ::
      corec
        (fun x =>
          match x with
          | (a, snd) => a)
        (fun p =>
          match p with
          | (l', s') => (l' ++ [head s'], tail s'))
        (l ++ [head s], tail s)
α : Type u
β : Type v
δ : Type w
l : List α
s : Stream' α
⊢ initsCore l s = l :: initsCore (l ++ [head s]) (tail s)
unfold initsCore corecOn
no goals
α : Type u
β : Type v
δ : Type w
l : List α
s : Stream' α
⊢ corec
      (fun x =>
        match x with
        | (a, snd) => a)
      (fun p =>
        match p with
        | (l', s') => (l' ++ [head s'], tail s'))
      (l, s) =
    l ::
      corec
        (fun x =>
          match x with
          | (a, snd) => a)
        (fun p =>
          match p with
          | (l', s') => (l' ++ [head s'], tail s'))
        (l ++ [head s], tail s)
rw [corec_eq]