proposition: Lemma list_permut_occurs_in_term_list : forall v l1 l2, permut l1 l2 -> occurs_in_term_list v l1 -> occurs_in_term_list v l2.
proof: Proof. intros v; cut (forall l l', occurs_in_term_list v l' -> occurs_in_term_list v (l ++ l')). intros H l1; induction l1. contradiction. intros l2 P O. assert (a_in_l2 : In a l2). rewrite <- (list_permut.in_permut_in P); left; trivial. destruct (In_split _ _ a_in_l2) as [l2' [l2'' H']]; subst l2. elim O; clear O; intro O. apply H; left; trivial. rewrite <- permut_cons_inside in P. generalize (IHl1 (l2' ++ l2'') P O). clear l1 IHl1 P O; induction l2'. intro; right; trivial. simpl; intro O; destruct O as [ O | O ]. left; trivial. right; apply IHl2'; trivial; apply in_or_app; right; left; trivial. reflexivity. intro l; induction l; trivial; right; apply IHl; trivial. Qed.
imports: Coq(Arith List) CoLoR(more_list list_sort term_spec ac cf_eq_ac)