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. intros t; destruct t as [ x | f l ]; trivial. intros [Wl A]; split; trivial. clear A; induction l as [ | t l]. contradiction. generalize Wl; clear Wl; intros [Wa Wl] u [Eq_u_a | In_u]. subst u; trivial. apply IHl; trivial. Qed.
imports: List more_list list_permut list_set Arith