proposition: Lemma rel_map_in_inv : forall (A B : Type)(rel : A -> B -> Prop) lsa lsb, rel_map rel lsa lsb -> forall a, In a lsa -> exists b, In b lsb /\ rel a b.
proof: Proof. induction 1; intuition; simpl in *. intuition. intuition; subst. econstructor; eauto. edestruct IHrel_map; eauto. intuition. econstructor; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation