proposition: Lemma cat_injr (A : Type) (a: seq A) : injective (cat ^~a).
proof: Proof. elim: a => [s1 s2 |b l IH s1 s2]; first by rewrite !cats0. by rewrite -!cat_rcons => /IH; apply: rcons_injr. Qed.
imports: mathcomp(all_ssreflect finmap)