proposition: Lemma lexprod_wf : well_founded LexProd_Lt.
proof: Proof. unfold well_founded; intro x. destruct x as [a b]; gen b. apply well_founded_ind with (R := ltL) (P := fun A => forall B, Acc_LexProd (A, B)); trivial. intros l wf_l. apply well_founded_ind with (R := ltR) (P := fun B => Acc_LexProd (l, B)); trivial. intros r wf_r. constructor; intros p p_lt; inversion p_lt. apply wf_l; auto with sets. fold Acc_LexProd. cut (eqPair (a',b') (l,b')). intro. apply (proj2 (Acc_LexProd_morph H4)). apply wf_r. hyp. auto with sets. Qed.
imports: CoLoR(LogicUtil RelUtil RelExtras) Coq(Setoid Morphisms Basics)