proposition: Lemma slist1_prop a (s := slist1 a): slistpl s \1c /\ Vg s \0c = a.
proof: Proof. have i01 := set1_1 \0c. have h: slistp (Lg \1c (fun _ : Set => a)) by split; aw;fprops. by rewrite/s/slistpl/slist1 /slength Lgd !LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)