proposition: Lemma symb_in_subterm : forall f s t p, subterm_at_pos t p = Some s -> symb_in_term f s = true -> symb_in_term f t = true.
proof: Proof. fix symb_in_subterm 4. intros f s t p; case p; clear p; simpl. intro H; injection H; clear H; intro H; rewrite H; intro H'; exact H'. intros n p; case t; clear t. intros v Abs; discriminate. intros g l; generalize (nth_error_ok_in n l); case (nth_error l n). intros tn H; case (H tn (eq_refl _)). intros l1 H'; case H'; clear H'. intros l2 H'; case H'; clear H'. intros L H' Sub f_in_s. rewrite symb_in_term_unfold. case (eq_symb_bool f g). reflexivity. simpl; rewrite H'; rewrite symb_in_term_list_app. case (symb_in_term_list f l1). reflexivity. simpl. rewrite (symb_in_subterm f s tn p Sub f_in_s); reflexivity. intros _ Abs; discriminate. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)