proposition: Lemma eq_inv_consK (a : S) u (b : T) v : eq_inv (a :: u) (b :: v) -> eq_inv u v.
proof: Proof. rewrite /eq_inv /versions => H i j. by move/(_ i.+1 j.+1) : H; rewrite !ltnS. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp