proposition: Lemma subRelGoodR : forall (A B : Type) (R : Rel A) (S : Rel B) (f : A -> B), (forall a b : A, R a b -> S (f a) (f b)) -> forall l : list A, GoodR A R l -> GoodR B S (map f l).
proof: Proof. intros A B R S f H' l H'0; elim H'0; simpl in |- *; auto. intros a l0 H'1; apply FoundG; auto. apply subPredExistsL with (P := fun x : A => R x a); auto. Qed.
imports: Coq(List)