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

State before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
wf_rel : s.σ → s.σ → Prop
q : { x // s.valid x = true }
i : Lex (ι × Bool)
⊢ wf_rel (s.seek q i) ↑q ∨ i < Stream.toOrder s q ∧ s.seek q i = ↑q ↔
    wf_rel (Stream.seek' s (↑q) i) ↑q ∨ coeLex i < Stream.toOrder' s ↑q ∧ Stream.seek' s (↑q) i = ↑q
Tactic:
simp only [Stream.seek'_val q.prop, Stream.coeLex_toOrder, coeLex_lt_iff]
State after:
no goals