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. intros sigma W_sigma t; pattern t; apply term_rec3. intros v _; simpl; generalize (W_sigma v); destruct (find eq_variable_dec v sigma); trivial. intros f l Hrec [Wl A]; split. clear A; induction l as [ | a l]; simpl; trivial; inversion_clear Wl as [Wa Wl']; split. apply Hrec; trivial; left; trivial. apply IHl; trivial; intros; apply Hrec; trivial; right; trivial. rewrite length_map; trivial. Qed.
imports: List more_list list_permut list_set Arith