proposition: Lemma rel_map_permutation : forall (A B : Type) lsa1 lsa2, Permutation lsa1 lsa2 -> forall (rel : A -> B -> Prop), (forall a b1 b2, rel a b1 -> rel a b2 -> b1 = b2) -> (forall a, exists b, rel a b) -> forall lsb1 lsb2, rel_map rel lsa1 lsb1 -> rel_map rel lsa2 lsb2 -> Permutation lsb1 lsb2.
proof: Proof. induction 1; intuition; simpl in *. inversion H1; clear H1; subst. inversion H2; clear H2; subst. econstructor. inversion H2; clear H2; subst. inversion H3; clear H3; subst. assert (b = b0). eapply H0; eauto. subst. eapply perm_skip. eauto. inversion H1; clear H1; subst. inversion H5; clear H5; subst. inversion H2; clear H2; subst. inversion H5; clear H5; subst. assert (b0 = b1); eauto; subst. assert (b = b2); eauto; subst. eapply perm_trans. eapply perm_swap. eapply perm_skip. eapply perm_skip. eauto. assert (lsb0 = lsb1). eapply rel_map_func; eauto. subst. eapply Permutation_refl. edestruct rel_map_left_total; eauto. eapply perm_trans. eapply IHPermutation1; eauto. eapply IHPermutation2; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation