proposition: Lemma slist_extent f g : slistp f -> slistp g -> slength f = slength g -> (forall i, \1c <=c i -> i <=c slength f -> (Vl f i = Vl g i)) -> f = g.
proof: Proof. move => fl gl eq1 sv. have sd: domain f = domain g by rewrite (slist_domain fl) (slist_domain gl) eq1. have dp:= (slist_domainP fl). have nN:= (slength_nat fl). move: fl gl => [ha _] [ha' _]. apply:fgraph_exten => // i /dp id. have ic:=(proj31_1 id). rewrite (Vl_correct f ic) (Vl_correct g ic). apply: sv; first by rewrite - succ_zero; apply: cleSS; apply:cle0x. by apply /(cleSlt0P ic). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)