proposition: Lemma fixedSpace_id : fixedSpace \1 = {:vT}%VS.
proof: Proof. by apply/vspaceP=> x; rewrite memvf; apply/fixedSpaceP; rewrite lfunE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)