proposition: Lemma defined_subterms_accumulates : forall is_def lhs x acc y, In y acc -> In y (defined_subterms is_def lhs acc x).
proof: Proof. intros is_def lhs x; induction x using term_rec3; intros acc y y_in_acc; simpl; trivial. apply fold_left_in_acc. intros acc0 x y0 H1 H2; apply H;auto with *. case (is_def f); [ | assumption]. case (eq_bool lhs (Term f l)). right; assumption. destruct (is_subterm (Term f l) lhs). assumption. right; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)