Theorem: Etch.Verification.Stream.IsStrictMono.evalOption_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
⊢ evalOption s (↑q) (s.index q) = some (s.value { val := q, property := hr })
Tactic:
simp [evalOption, h.evalMultiset_ready hr]
State after:
no goals