proposition: Theorem AccElim2 : forall (A B:Set) (RA: A -> A -> Prop) (RB: B -> B -> Prop), forall (P : A -> B -> Prop), (forall x y, (forall (t : A), RA t x -> forall y', Acc RB y' -> P t y') -> (forall (t : B), RB t y -> P x t) -> (P x y)) -> forall x y, Acc RA x -> Acc RB y -> P x y.
proof: Proof. intros A B RA RB P H x y Ax; generalize y; clear y. elim Ax. clear Ax x; intros x HAccx Hrecx y Ay. elim Ay. clear Ay y. intros y HAccy Hrecy. apply H. auto. auto. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef