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