proposition: Lemma well_formed_cf_fold : forall t, (match t with | Var _ => True | Term f l => (forall u, In u l -> well_formed_cf u) /\ (match arity f with | AC => length l >= 2 /\ is_sorted l /\ (forall u, In u l -> match u with | Var _ => True | Term g _ => f <> g end) | C => length l = 2 /\ is_sorted l | Free n => length l = n end) end) -> well_formed_cf t.
proof: Proof. intro t; destruct t as [v | f l]; trivial. intros [Wl Hl]; split; trivial; clear Hl; induction l as [ | t l]; intuition; apply IHl; intros; apply Wl; right; trivial. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)