proposition: Lemma symb_in_direct_subterm : forall f l t g, In t l -> symb_in_term g t = true -> symb_in_term g (Term f l) = true.
proof: Proof. intros f l s g s_in_l g_in_s; rewrite symb_in_term_unfold. case (eq_symb_bool g f). reflexivity. simpl; revert l s_in_l; fix symb_in_direct_subterm 1. intro l; case l; clear l. intro Abs; elim Abs. simpl In; intros t l s_in_tl; case s_in_tl; clear s_in_tl. intros t_eq_s; subst t; simpl; rewrite g_in_s; reflexivity. intros s_in_l; simpl; case (symb_in_term g t). reflexivity. rewrite (symb_in_direct_subterm _ s_in_l); reflexivity. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)