proposition: Lemma eq_inv_size d1 d2 (T1 : inhOrderType d1) (T2 : inhOrderType d2) (w1 : seq T1) (w2 : seq T2) : eq_inv w1 w2 -> size w1 = size w2.
proof: Proof. move=> Hinv. wlog suff Hwlog : d1 T1 d2 T2 w1 w2 Hinv / size w1 <= size w2. by apply anti_leq; rewrite !Hwlog. rewrite /eq_inv /versions in Hinv. case H : (size w1) => [// | n]. move/(_ n n) : Hinv; rewrite H leqnn ltnSn lexx /=. by move/eqP/andP => []. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp