proposition: Lemma map_nilp {A B} (f : A -> B) (s : seq A) : nilp (map f s) = nilp s.
proof: Proof. by rewrite /nilp; case: s. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)