proposition: Lemma fold_left_defined_subterms_unfold : forall is_def lhs l acc t, In t (fold_left (defined_subterms is_def lhs) l acc) <-> In t (fold_left (defined_subterms is_def lhs) l nil) \/ In t acc.
proof: Proof. intros is_def lhs l; induction l as [ | s l]. intros acc t; simpl; split; [intro H; right; exact H | intros [Abs | H]; [contradiction | exact H]]. simpl; intros acc t. rewrite (IHl (defined_subterms is_def lhs acc s)). rewrite (IHl (defined_subterms is_def lhs nil s)). rewrite defined_subterms_unfold. intuition. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)