proposition: Lemma slist_append_list x y: slistp x -> slistp y -> slistp (slist_append x y) /\ slength (slist_append x y) = slength x +c slength y.
proof: Proof. move=> ha hb. move:(slength_nat ha)(slength_nat hb) => nN mN. have nmM:=(NS_sum nN mN). have d: (domain (slist_append x y)) = (slength x +c slength y). by rewrite /slist_append; aw. by rewrite /slistp /slength d; split => //; split => //; apply:Lg_fgraph. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)