fact: Definition unpack K (k : forall T (c : class_of T), K T c) cT := let: Pack T c _ := cT return K _ (class cT) in k _ c.
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)