rintro ⟨acc, _⟩ ⟨_, x⟩ ⟨⟨⟩, ⟨⟩⟩
case hf
α : 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) →
      a.fst = a'.fst
case hf.mk.mk.intro.refl.refl
α : Type u_1
σ : Stream' α
x✝ : α
f : α → ℕ
g : α → α
acc : ℕ
x : α
⊢ (acc, corec f g x).fst = (acc, x).fst