proposition: Lemma well_formed_unfold : forall t, well_formed t -> match t with | Var _ => True | Term f l => (forall u, In u l -> well_formed u) /\ (match arity f with | Free n => length l = n | _ => length l = 2 end) end.
proof: Proof. unfold well_formed. intros t; destruct t as [ x | f l ]; trivial. simpl; rewrite Bool.andb_true_iff. intros [Wl Ar]; split. clear Ar; induction l as [ | t l]. intros u Abs; elim Abs. rewrite Bool.andb_true_iff in Wl. destruct Wl as [Wa Wl]; intros u [Eq_u_a | In_u]. subst u; trivial. apply IHl; trivial. revert Ar; case (arity f); intros; apply Nat.eqb_eq; assumption. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)