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

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
q : { q // s.valid q = true }
hr : s.ready q = true
⊢ (evalMultiset s ↑q) (s.index q) = {s.value { val := q, property := hr }}
Tactic:
simp [h.evalMultiset_advance_of_ready hr, hr, -advance_val]
State after:
no goals