fact: Definition defaultEncModRelClass := @EncModRelClassPack D D id id r r (fun _ rxx => rxx) (fun _ _ => erefl _).
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice) mathcomp(seq fintype)