Theorem: Etch.Verification.Stream.zip_spec' (Etch/StreamFusion/Proofs/StreamZip.lean)

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (zip a b).σ
i : ι
⊢ (evalMultiset (zip a b) q) i =
    Option.getD (Option.map (fun x => {x}) (Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i))) 0
Tactic:
rw [(zip_strict_mono a.strictMono b.strictMono ).evalMultiset_eq_evalOption, zip_spec]
State after:
no goals