proposition: Lemma acc_and : forall A B (R1 : relation A) (R2 : relation B), forall a b, Acc R1 a -> Acc R2 b -> Acc (product_o R1 R2) (a,b).
proof: Proof. intros A B R1 R2 a b Acc_a; generalize b; clear b; induction Acc_a as [a Acc_a IHa]. intros b Acc_b; generalize a Acc_a IHa; clear a Acc_a IHa; induction Acc_b as [b Acc_b IHb]; intros a Acc_a IHa; apply Acc_intro; intros [a' b'] H; inversion H; clear H; subst. apply IHa; trivial. apply Acc_intro; trivial. apply IHb; trivial. Defined.
imports: Coq(Setoid Relations List Wellfounded)