simp only [head_corec, tail_corec, and_self]
case hg.mk.mk.intro.refl.refl
α : Type u_1
σ : Stream' α
x✝ : α
f : α → ℕ
g : α → α
acc : ℕ
x : α
⊢ match ((acc, corec f g x).fst + head (acc, corec f g x).snd, tail (acc, corec f g x).snd) with
  | (acc₁, σ) =>
    match ((acc, x).fst + f (acc, x).snd, g (acc, x).snd) with
    | (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x
no goals