proposition: Lemma OpenInd : forall xs : list A, Min xs -> (forall a : A, Min (a :: xs) -> GRBar A R (a :: xs)) -> GRBar A R xs.
proof: Proof. Proof using wflt. intros; red in |- *. apply Ind; auto. intros a; elim (wflt a); auto. intros x H' H'0. apply X0. apply cmin; auto. Qed.
imports: Coq(List) Buchberger(Bar)