proposition: Lemma ffunE g x : (finfun g : fT) x = g x.
proof: Proof. rewrite unlock /=; set s := enum aT; set s_x : mem_seq s x := mem_enum _ _. by elim: s s_x => //= x1 s IHs; case: eqP => [|_]; [case: x1 / | apply: IHs]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple)