proposition: Lemma symb_in_term_list_app : forall f l1 l2, symb_in_term_list f (l1 ++ l2) = orb (symb_in_term_list f l1) (symb_in_term_list f l2).
proof: Proof. fix symb_in_term_list_app 2. intros f l1 l2; case l1; clear l1; simpl. reflexivity. intros t l1; rewrite <- Bool.orb_assoc. apply (f_equal (fun b => orb (symb_in_term f t) b)). apply symb_in_term_list_app. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)