proposition: Theorem well_formed_apply_subst : forall sigma, well_formed_subst sigma -> forall t, well_formed t -> well_formed (apply_subst sigma t).
proof: Proof. unfold well_formed. intros sigma W_sigma t; pattern t; apply term_rec3. intros v _; simpl; generalize (W_sigma v); destruct (find eq_var_bool v sigma); trivial. intros f l Hrec; simpl; rewrite Bool.andb_true_iff; intros [Wl Ar]. rewrite Bool.andb_true_iff; split. clear Ar; induction l as [ | a l]; simpl; trivial. rewrite Bool.andb_true_iff in Wl; destruct Wl as [Wa Wl']. rewrite Bool.andb_true_iff; split. apply Hrec; trivial; left; trivial. apply IHl; trivial; intros; apply Hrec; trivial; right; trivial. rewrite length_map; trivial. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)