proposition: Lemma monGRBarAux : forall (A : Type) (R : Rel A) (l : list A), GRBar A R l -> forall xs bs cs : list A, l = xs ++ cs -> GRBar A R (xs ++ bs ++ cs).
proof: Proof. intros A R l H'; elim H'; auto. intros l0 H'0 xs bs cs H'1; red in |- *; rewrite H'1 in H'0; auto. intros l0 H'0 H'1 xs bs cs H'2; rewrite H'2 in H'1; auto. red in |- *; apply Ind. intros a. change (Bar A (GoodR A R) ((a :: xs) ++ bs ++ cs)) in |- *. unfold GRBar in H'1; apply H'1 with (a := a); auto. Qed.
imports: Coq(List)