proposition: Lemma monGoodR : forall (A : Type) (R : Rel A) (xs bs cs : list A), GoodR A R (xs ++ bs) -> GoodR A R (xs ++ cs ++ bs).
proof: Proof. intros A R xs bs cs; elim xs; simpl in |- *; auto. intros a l H' H'0; inversion H'0; simpl in |- *; auto. Qed.
imports: Coq(List)