Theorem: Etch.Verification.Stream.ready'_val (Etch/StreamFusion/Proofs/StreamProof.lean)

State before:
ι : Type
α : Type u_1
a b s : Stream ι α
x : { q // s.valid q = true }
⊢ ready' s ↑x ↔ s.ready x = true
Tactic:
simp [Stream.ready', x.prop]
State after:
no goals