proposition: Lemma rel_map_unary_pred : forall (A B : Type)(P : A -> B -> Prop)(lsa : list A)(lsb : list B)(P' : B -> Prop), rel_map P lsa lsb -> (forall a b, P a b -> P' b) -> forall b, In b lsb -> P' b.
proof: Proof. induction 1; intuition; simpl in *. intuition. intuition; subst. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation