proposition: Theorem jjProp1 : forall (d : nat) (m : mon d), d = 0 -> m = jj d.
proof: Proof. intros d m; elim m. simpl in |- *; auto. intros d0 n m0 H' H'0; inversion H'0. Qed.
imports: Coq(List PeanoNat Wf_nat Inverse_Image) Buchberger(Bar OpenIndGoodRel Monomials)