proposition: Lemma rel_map_func : forall (A B : Type) (rel : A -> B -> Prop) lsa lsb1, rel_map rel lsa lsb1 -> forall lsb2, rel_map rel lsa lsb2 -> (forall a b1 b2, In a lsa -> rel a b1 -> rel a b2 -> b1 = b2) -> lsb1 = lsb2.
proof: Proof. induction 1; intuition; simpl in *. inversion H; clear H; subst. trivial. inversion H1; clear H1; subst. f_equal. eauto. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation