proposition: Lemma slist_emptyp l: slistp l -> slength l = \0c -> l = emptyset.
proof: Proof. move => sa sb. move: (slist_domain sa); rewrite sb Nint_co00 => dle. by apply/set0_P => x /domain_i1; rewrite dle => /in_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)