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

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