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

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