proposition: Lemma wf_lex : forall A B (eq_bool : A -> A -> bool) o1 o2 (eq_bool_ok : forall a1 a2, if eq_bool a1 a2 then a1 = a2 else a1 <> a2), well_founded o1 -> well_founded o2 -> well_founded (@lex A B eq_bool o1 o2).
proof: Proof. intros A B eq_bool o1 o2 eq_bool_ok W1 W2. intros [a1 a2]; revert a2; generalize (W1 a1); intros Wa1 a2; generalize (W2 a2). revert a2; induction Wa1 as [a1 Wa1 wf_lex]. intros a2 Wa2. revert a1 Wa1 wf_lex. revert a2 Wa2; fix wf_lex2 2. intros a2 Wa2 a1 Wa1 wf_lex. apply Acc_intro; intros [b1 b2]; simpl. generalize (eq_bool_ok b1 a1); case (eq_bool b1 a1); [intro b1_eq_a1 | intro b1_diff_a1]. intros b2_lt_a2; rewrite b1_eq_a1. apply (wf_lex2 b2 (Acc_inv Wa2 b2_lt_a2) a1 Wa1 wf_lex). intro b1_lt_a1; exact (wf_lex b1 b1_lt_a1 _ (W2 b2)). Defined.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)