proposition: Lemma eq_inv_nil : eq_inv (@nil S) (@nil T).
proof: Proof. rewrite /eq_inv /versions => i j /=. by rewrite ltn0 andbF. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp