proposition: Lemma free_uniq X : free X -> uniq X.
proof: Proof. elim: X => //= v b IH_X; rewrite free_cons => /andP[X'v /IH_X->]. by rewrite (contra _ X'v) // => /memv_span. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)