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

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
h : ¬s.valid q = true
⊢ evalOption s q i = none
Tactic:
simp [Stream.evalOption, h]
State after:
no goals