proposition: Lemma well_formed_fold : forall 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 -> well_formed t.
proof: Proof. intros t; destruct t as [ x | f l ]; trivial. intros [Wl A]; split ; trivial; clear A; induction l as [ | t l]; trivial; split. apply Wl; left; trivial. apply IHl; intros; apply Wl; right; trivial. Qed.
imports: List more_list list_permut list_set Arith