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

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