Theorem: Stream'.tail_corec (ListPowersProblem/StreamLemmas.lean)

State before:
α : Type ?u.6271
σ : Stream' α
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
g : α✝¹ → α✝¹
x : α✝¹
⊢ tail (corec f g x) = corec f g (g x)
Tactic:
simp only [tail, nth, corec_succ]
State after:
no goals