proposition: Lemma well_formed_apply_subst_strong : forall sigma t, (forall x, var_in_term x t = true -> well_formed (apply_subst sigma (Var x))) -> well_formed t -> well_formed (apply_subst sigma t).
proof: Proof. intros sigma t; pattern t; apply term_rec3; clear t. intros v W_sigma _; apply W_sigma; simpl. rewrite eq_var_bool_refl; apply eq_refl. intros f l IHl W_sigma Wfl. destruct (well_formed_unfold Wfl) as [Wl Af]; clear Wfl. apply well_formed_fold; split. intros u u_in_mapl; rewrite in_map_iff in u_in_mapl; destruct u_in_mapl as [t [H t_in_l]]. subst u; apply IHl; trivial. intros v v_in_t; apply W_sigma; rewrite var_in_term_is_sound. destruct (in_split_set _ eq_bool_ok _ _ t_in_l) as [l' [l'' H]]; subst l. rewrite var_list_unfold; rewrite var_list_list_app; apply in_or_app; right. apply in_or_app; left; rewrite <- var_in_term_is_sound; assumption. apply Wl; assumption. rewrite map_length; assumption. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)