proposition: Lemma rel_map_eq_inv : forall (A B : Type)(ls1 ls2 : list A)(rel1 rel2 : A -> B -> Prop) ls1' ls2', ls1 = ls2 -> (forall a b1 b2, rel1 a b1 -> rel2 a b2 -> b1 = b2) -> rel_map rel1 ls1 ls1' -> rel_map rel2 ls2 ls2' -> ls1' = ls2'.
proof: Proof. induction ls1; intuition; subst. inversion H1; clear H1; subst. inversion H2; clear H2; subst. trivial. inversion H1; clear H1; subst. inversion H2; clear H2; subst. f_equal. eapply H0; eauto. eapply IHls1; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation