proposition: Lemma NoDup_map_ext {X Y : Type} (f : X -> Y) (l : list X) : (forall x1, In x1 l -> forall x2, In x2 l -> f x1 = f x2 -> x1 = x2) -> NoDup l -> NoDup (map f l).
proof: Proof. elim: l. { move=> *. by constructor. } move=> x l IH /= H /NoDup_cons_iff [Hxl] /IH {}IH. constructor. - move=> /in_map_iff [x'] [/H] ? Hx'l. have ? : x' = x by tauto. subst x'. exact: (Hxl Hx'l). - apply: IH. move=> x1 Hx1l x2 Hx2l /H. tauto. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun