proposition: Lemma lem1 : forall us : list (A * B), GoodR B R (sndL us) -> MinD us -> GBarlR us.
proof: Proof. Proof using declt. intros us H' H'0. apply lem1aux with (l := sndL us); auto. Qed.
imports: Coq(List PeanoNat Wf_nat Inverse_Image) Buchberger(Bar OpenIndGoodRel Monomials)