proposition: Theorem nat_double_ind_set : forall R : nat -> nat -> Type, (forall n : nat, R 0 n) -> (forall n : nat, R (S n) 0) -> (forall n m : nat, R n m -> R (S n) (S m)) -> forall n m : nat, R n m.
proof: Proof. simple induction n; simple induction m; auto. Qed.
imports: Coq(List PeanoNat Wf_nat Inverse_Image) Buchberger(Bar OpenIndGoodRel Monomials)