proposition: Lemma not_in_map : forall (A B : Set)(ls : list A)(f : A -> B)(f_inv : B -> A)(a : A), (forall a, f_inv (f a) = a) -> ~In a ls -> ~In (f a) (map f ls).
proof: Proof. induction ls; intuition. simpl in *. intuition. eapply H1. rewrite <- (H a). rewrite <- (H a0). f_equal. trivial. eapply IHls; eauto. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia