proposition: Theorem wf_R_pair : well_founded R_pair.
proof: Proof. red. intro x. destruct x. generalize dependent u. apply (well_founded_ind wf_RT (fun t => forall u : U, Acc R_pair (t, u))) . do 2 intro. apply (well_founded_ind wf_RU (fun u => Acc R_pair (x,u))). intros. constructor. destruct y. remember (t0,u). remember (x,x0). inversion 1; subst; inversion H4; inversion H3; clear H4 H3; subst; eauto. Defined.
imports: Coq.Relations.Relation_Definitions Coq.Classes.RelationClasses ExtLib.Core.RelDec ExtLib.Tactics.Consider ExtLib.Tactics.Injection