proposition: Lemma perm_map_in : forall (A B : Set)(lsa : list A)(lsb : list B)(f : A -> B)(f_inv : B -> A), (forall b, In b lsb -> f (f_inv b) = b) -> (forall a, In a lsa <-> In (f a) lsb) -> NoDup (map f lsa) -> NoDup lsb -> Permutation (map f lsa) lsb.
proof: Proof. intuition. eapply NoDup_Permutation; intuition. apply in_map_iff in H3. destruct H3. intuition. subst. eapply H0. trivial. eapply in_map_iff. econstructor. split. 2:{ eapply H0. assert (x = f (f_inv x)). symmetry. eapply H. trivial. rewrite H4 in H3. eapply H3. } eapply H. trivial. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia