proposition: Lemma well_formed_cf_subterms : forall f l, well_formed_cf (Term f l) -> (forall t, In t l -> well_formed_cf t).
proof: Proof. intros f l W; elim (well_formed_cf_unfold _ W); trivial. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)