proposition: Lemma subType_seqP : map val subType_seq = subenum.
proof: Proof. rewrite /subType_seq; elim: subenum subenumP => [|l0 l IHl] //=. by case/andP => /= H0 Hall0; rewrite insubT /= IHl // SubK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools