proposition: Lemma equiv_eval_lists: forall A ll n rpo_infos, (forall t1 t2, In (t1, t2) ll -> equiv_eval rpo_infos n t1 t2 = Some true) -> permut0 equiv (A ++ map (fun st : term * term => fst st) ll) (A ++ map (fun st : term * term => snd st) ll).
proof: Proof. intro H. induction ll. intros n rpo_infos H1. simpl. apply permut_refl. intros a H'. reflexivity. intros. assert (H':= IHll n rpo_infos); clear IHll. assert (H1: permut0 equiv (H ++ map (fun st : term * term => fst st) ll) (H ++ map (fun st : term * term => snd st) ll)). apply H'. intros t1 t2 H3. assert (H0':= H0 t1 t2). apply H0'. simpl. right; assumption. assert (H0':= H0 (fst a) (snd a)); clear H0. assert (equiv_eval rpo_infos n (fst a) (snd a) = Some true). apply H0'. simpl; left. destruct a. simpl. trivial. simpl. apply permut_strong. assert (H1':= equiv_eval_is_sound_weak). assert (H2:= H1' rpo_infos n (fst a) (snd a)). apply H2; trivial. trivial. 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)