proposition: Lemma in_symb_list_list : forall l f, In f (symb_list_list l) -> exists t, In t l /\ In f (symb_list t).
proof: Proof. fix in_symb_list_list 1; intro l; case l; clear l. intros v v_in_nil; contradiction. simpl; intros t l v v_in_tl; destruct (in_app_or _ _ _ v_in_tl) as [v_in_t | v_in_l]. exists t; split; [left; apply eq_refl | assumption]. destruct (in_symb_list_list l v v_in_l) as [u [u_in_l v_in_u]]. exists u; split; [right | idtac]; assumption. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)