Theorem: Etch.Verification.Stream.eval_map_id (Etch/StreamFusion/Proofs/StreamProof.lean)

State before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddZeroClass α
f : α → α
hf : f = id
s : Stream ι α
inst✝ : IsBounded s
⊢ eval (map f s) = eval s
Tactic:
subst f
State after:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
⊢ eval (map id s) = eval s

State before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
⊢ eval (map id s) = eval s
Tactic:
rfl
State after:
no goals