Theorem: Etch.Verification.Stream.toOrder'_val (Etch/StreamFusion/Proofs/StreamProof.lean)

State before:
ι : Type
α : Type u_1
a b s : Stream ι α
q : { q // s.valid q = true }
⊢ toOrder' s ↑q = (index' s ↑q, s.ready q)
Tactic:
simp [Stream.toOrder']
State after:
no goals