proposition: Lemma monGRBar : forall (A : Type) (R : Rel A) (xs bs cs : list A), GRBar A R (xs ++ cs) -> GRBar A R (xs ++ bs ++ cs).
proof: Proof. intros A R xs bs cs H'. apply monGRBarAux with (l := xs ++ cs); auto. Qed.
imports: Coq(List)