proposition: Lemma map_eqr (T1 T2 : eqType) (f : T1 -> T2) (s1 s2 : seq T1) : injective f -> ([seq f i | i <- s1] == [seq f i | i <- s2]) = (s1 == s2).
proof: Proof. elim: s1 s2 => [[|] //|a s1 IH [|b s2]//=] fInj. rewrite !eqseq_cons IH //. case: (a =P b) => [->//|]; first by rewrite eqxx. by case: (f a =P f b) => [/fInj|//]. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)