proposition: Lemma map_NoDup : forall (A B : Set)(ls : list A)(f : A -> B)(f_inv : B -> A), (forall a, In a ls -> f_inv (f a) = a) -> NoDup ls -> NoDup (map f ls).
proof: Proof. induction ls; intuition; simpl in *. econstructor. inversion H0; clear H0; subst. econstructor; eauto. intuition. apply in_map_iff in H0. destruct H0. intuition. assert (x = a). rewrite <- (H x); intuition. rewrite <- (H a); intuition. f_equal. trivial. subst. intuition. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia