proposition: Lemma symb_list_list_ok : forall f l, In f (symb_list_list l) <-> symb_in_term_list f l = true.
proof: Proof. intros f l; induction l as [ | t l]; split; intro H. contradiction. discriminate. simpl; simpl in H; destruct (in_app_or _ _ _ H) as [Ht | Hl]. rewrite symb_list_ok in Ht; rewrite Ht; apply eq_refl. rewrite IHl in Hl; rewrite Hl; case (symb_in_term f t); apply eq_refl. simpl; simpl in H. case_eq (symb_in_term f t); [intro f_in_t | intro f_not_in_t]. apply in_or_app; left; rewrite symb_list_ok; assumption. apply in_or_app; right; rewrite IHl; rewrite f_not_in_t in H; assumption. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)