proposition: Lemma rel_map_impl : forall (A B : Type)(rel1 rel2 : A -> B -> Prop) lsa lsb, rel_map rel1 lsa lsb -> (forall a b, In a lsa -> rel1 a b -> rel2 a b) -> rel_map rel2 lsa lsb.
proof: Proof. induction lsa; intuition. inversion H; clear H; subst. econstructor. inversion H; clear H; subst. econstructor. eapply IHlsa; eauto. intuition. eapply H0. simpl. intuition. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation