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

State before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
hr : s.ready q = true
⊢ (evalMultiset s ↑q) (s.index q) =
    insert (s.value { val := q, property := hr }) ((evalMultiset s (advance s ↑q)) (s.index q))
Tactic:
simp [Stream.evalMultiset, Stream.eval₀, hr]
State after:
no goals