proposition: Lemma fmap_map_seqZ {B} (f : A → B) start xs : f <$> map_seqZ start xs =@{M B} map_seqZ start (f <$> xs).
proof: Proof. revert start. induction xs as [|x xs IH]; intros start; csimpl. { by rewrite fmap_empty. } by rewrite fmap_insert, IH. Qed.
imports: Coq(Permutation) stdpp(options)