proposition: Lemma freeE n (X : n.-tuple vT) : free X = [forall i : 'I_n, X`_i \notin <<drop i.+1 X>>%VS].
proof: Proof. case: X => X /= /eqP <-{n}; rewrite -(big_andE xpredT) /=. elim: X => [|v X IH_X] /=; first by rewrite nil_free big_ord0. by rewrite free_cons IH_X big_ord_recl drop0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)