rintro ⟨acc, _⟩ ⟨_, x⟩ ⟨⟨⟩, ⟨⟩⟩
case hg
α : Type u_1
σ : Stream' α
x : α
f : α → ℕ
g : α → α
⊢ ∀ (a : ℕ × Stream' ℕ) (a' : ℕ × α),
    (match a with
      | (acc₁, σ) =>
        match a' with
        | (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x) →
      match (a.fst + head a.snd, tail a.snd) with
      | (acc₁, σ) =>
        match (a'.fst + f a'.snd, g a'.snd) with
        | (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x
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