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

State before:
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
β : Type u_2
s : Stream ι α
f : α → β
⊢ IsMonotonic (map f s) ↔ IsMonotonic s
Tactic:
rfl
State after:
no goals