proposition: Lemma subRelGRBar : 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 b : B, {a : A | b = f a}) -> forall l : list A, GRBar A R l -> GRBar B S (map f l).
proof: Proof. intros A B R S f H' H'0 l H'1; elim H'1; simpl in |- *; auto. intros l0 H'2. red in |- *; apply Base; auto. unfold GRBar in |- *. apply subRelGoodR with (R := R); auto. intros l0 H'2 H'3; red in |- *; apply Ind; auto. intros a; case (H'0 a); auto. intros x H'4; rewrite H'4; auto. unfold GRBar in H'3; apply H'3; auto. Qed.
imports: Coq(List)