proposition: Lemma permut0_mem : forall A X L b, permut0 eq A (X ++ L) -> mem equiv b X -> mem equiv b A.
proof: Proof. intros. assert (H1:= permut_impl). assert (H1':= H1 term term eq equiv A (X ++ L)); clear H1. assert (permut0 equiv A (X++L)). apply H1'. intros a b0 H2. rewrite H2. reflexivity. trivial. assert (H2:=mem_permut0_mem). assert (H2':= H2 term equiv). assert (forall (l1 l2 : list term) (a : term), permut0 equiv l1 l2 -> (mem equiv a l1 <-> mem equiv a l2)). apply H2'. apply equiv_equiv. assert (H3':= H3 A (X ++ L) b). assert (mem equiv b A <-> mem equiv b (X ++ L)). apply H3'. assumption. apply H4; clear H H1 H1' H2 H3 H4. generalize H0. generalize X. induction X0. intros. contradiction. simpl. intros. destruct H1. left; trivial. right. apply IHX0; 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)