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

State before:
ι : Type
α : Type ?u.6775
a b s : Stream ι α
inst✝ : Preorder ι
x y : StreamOrder ι
⊢ coeLex x < coeLex y ↔ x < y
Tactic:
simp [Prod.Lex.lt_iff']
State after:
no goals