proposition: Lemma mem_mem : forall t l1 l2, equiv_list_lex l1 l2 -> (mem equiv t l1 <-> mem equiv t l2).
proof: Proof. intros t l1 l2 l1_eq_l2; split. generalize t l2 l1_eq_l2; clear t l2 l1_eq_l2; induction l1 as [ | t1 l1]; intros t l2 l1_eq_l2 t_mem_l1. contradiction. inversion l1_eq_l2 as [ | s1 s2 l1' l2' s1_eq_s2 l1_eq_l2']; subst. destruct t_mem_l1 as [ t_eq_t1 | t_mem_l1]. left; transitivity t1; trivial. right; apply IHl1; trivial. generalize t l2 l1_eq_l2; clear t l2 l1_eq_l2; induction l1 as [ | t1 l1]; intros t l2 l1_eq_l2 t_mem_l2; inversion l1_eq_l2 as [ | s1 s2 l1' l2' s1_eq_s2 l1_eq_l2']; subst. trivial. destruct t_mem_l2 as [ t_eq_t2 | t_mem_l2]. left; transitivity s2; trivial. symmetry; trivial. right; apply IHl1 with l2'; 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)