proposition: Lemma subsetT_hint mA : subset mA (mem [set: T]).
proof: Proof. by rewrite unlock; apply/pred0P=> x; rewrite !inE in_set. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)