proposition: Lemma keylem : forall bs : list B, GRBar B R bs -> forall us : list (A * B), bs = sndL us -> MinD us -> GBarlR us.
proof: Proof. Proof using wfgt declt. intros bs H'; elim H'; auto. intros l H'0 us H'1 H'2. apply lem1; auto. rewrite <- H'1; auto. intros l H'0 H'1 us H'2 H'3; red in |- *. apply OpenInd with (lt := prod_lt); auto. exact WFlem1. intros a H'4. apply H'1 with (a := snd a); auto. rewrite H'2; auto. Qed.
imports: Coq(List PeanoNat Wf_nat Inverse_Image) Buchberger(Bar OpenIndGoodRel Monomials)