apply corec_bisim (fun (acc₁, σ) (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x)
α : Type u_1
σ : Stream' α
x : α
f : α → ℕ
g : α → α
⊢ corec Prod.fst (fun x => (x.fst + head x.snd, tail x.snd)) (f x, corec f g (g x)) =
    corec Prod.fst (fun x => (x.fst + f x.snd, g x.snd)) (f x, g 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 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 a
α : Type u_1
σ : Stream' α
x : α
f : α → ℕ
g : α → α
⊢ match (f x, corec f g (g x)) with
  | (acc₁, σ) =>
    match (f x, g x) with
    | (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x