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

State before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
⊢ eval s ↑q = eval₀ s q + eval s (advance s ↑q)
Tactic:
rw [Stream.eval, dif_pos]
State after:
no goals