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

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