proposition: Lemma mem_concat: forall a ls lc, mem equiv a (ls ++ lc) -> mem equiv a ls \/ mem equiv a lc.
proof: Proof. induction ls. simpl. intros. right; trivial. intros. simpl. simpl in H. destruct H. left; left; trivial. assert (H1:= IHls lc). assert (mem equiv a ls \/ mem equiv a lc). apply H1; trivial. tauto. 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)