proposition: Lemma set_of_nilp (T : choiceType) (s : seq T) : (set_of s == fset0) = (nilp s).
proof: Proof. apply/idP/nilP; last by rewrite fset0E;move->. apply: contraTeq. case: s => // a l _. apply/emptyPn; exists a. by rewrite set_ofE inE eqxx. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)