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. unfold well_formed. intros t; destruct t as [ x | f l ]; simpl; trivial. intros [Wl Ar]; rewrite Bool.andb_true_iff. split. clear Ar; induction l as [ | t l]; trivial. rewrite Bool.andb_true_iff; split. apply Wl; left; trivial. apply IHl; intros; apply Wl; right; trivial. revert Ar; case (arity f). intro Ar; rewrite Ar; apply Nat.eqb_refl; assumption. intro Ar; rewrite Ar; apply Nat.eqb_refl; assumption. intros n Ar; rewrite Ar; apply Nat.eqb_refl; assumption. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)