proposition: Lemma equiv_in_list : forall f g (f_stat : status Prec f= Lex) (g_stat: status Prec g = Lex) l1 l2, length l1 = length l2 -> prec_eq Prec f g -> (forall t1 t2, In (t1, t2) (combine l1 l2) -> equiv t1 t2) -> equiv (Term f l1) (Term g l2).
proof: Proof. intros f g f_stat g_stat l1 l2 L prec_eq_f_g E. apply (Eq_lex f g f_stat g_stat prec_eq_f_g). clear f f_stat prec_eq_f_g; revert l1 l2 L E; fix equiv_in_list 1; intro l1; case l1; clear l1. intros l2; case l2; clear l2. intros _ _; apply Eq_list_nil. intros a2 l2 L _; discriminate. intros a1 l1 l2; case l2; clear l2. intro L; discriminate. intros a2 l2 L E; apply Eq_list_cons. apply E; left; apply eq_refl. apply (equiv_in_list l1 l2). injection L; intros; assumption. intros t1 t2 H; apply E; right; assumption. Qed.
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)