proposition: Lemma slist_append_empty x: slistp x -> slist_append x emptyset = x.
proof: Proof. move => [fgx lx]. rewrite /slist_append /slength; aw; rewrite (csum0r (CS_nat lx)). apply: fgraph_exten; [ fprops | done | by aw | aw] => i idg. by rewrite (LgV idg) Y_true //; apply/(NltP lx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)