proposition: Lemma nilp_intersect (A : eqType) (s t : seq A) : nilp (intersect s t) = ~~ has (mem s) t.
proof: Proof. by rewrite /intersect /nilp size_filter has_count lt0n negbK. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib