proposition: Lemma std_eq_invP (u : seq S) (v : seq T) : reflect (eq_inv u v) (std u == std v).
proof: Proof. apply: (iffP idP). - move=> /eqP Heq; apply: (eq_inv_trans (eq_inv_std u)). by rewrite Heq; apply: eq_inv_sym; exact: eq_inv_std. - by move /std_eq_inv ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp