proposition: Lemma defined_subterms_unfold : forall is_def s lhs acc, forall t, In t (defined_subterms is_def lhs acc s) <-> (In t (defined_subterms is_def lhs nil s) \/ In t acc).
proof: Proof. intros is_def s lhs acc t. rewrite <- (defined_subterms_unfold_gen is_def s lhs nil acc nil acc). simpl; split; exact (fun H => H). intro; split; exact (fun H => H). intro; split; exact (fun H => H). Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)