proposition: Lemma wf_lex : forall (o1 lo1 o2 : relation term), (forall t1 t2 t3, o1 t1 t2 -> lo1 t2 t3 -> o1 t1 t3) -> well_founded o1 -> well_founded o2 -> well_founded (lex o1 lo1 o2).
proof: Proof. intros o1 lo1 o2 Transo W1 W2. intro t; apply (well_founded_ind W1); clear t. intro t; pattern t; apply (well_founded_ind W2); clear t. intros t IH2 IH1; apply Acc_intro. intros s H; inversion H as [u1 u2 K | u1 u2 K1 K2]; subst. apply IH1; assumption. apply IH2. assumption. intros u K3; apply IH1; apply Transo with s; assumption. Defined.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec)