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

State before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : { q // s.valid q = true }
⊢ WfRel s (advance s ↑q) ↑q
Tactic:
rw [Stream.advance_val]
State after:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : { q // s.valid q = true }
⊢ WfRel s (s.seek q (toOrder s q)) ↑q

State before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : { q // s.valid q = true }
⊢ WfRel s (s.seek q (toOrder s q)) ↑q
Tactic:
exact s.progress rfl.le
State after:
no goals