fact: Definition eq_inv d1 d2 (T1 : inhOrderType d1) (T2 : inhOrderType d2) (w1 : seq T1) (w2 : seq T2) := (versions w1) =2 (versions w2).
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp