proposition: Lemma well_formed_remove_subst : forall sigma t, well_formed (apply_subst sigma t) -> well_formed t.
proof: Proof. intros sigma t; pattern t; apply term_rec3; clear t. intros v _; apply eq_refl. intros f l Hrec Wfl; destruct (well_formed_unfold Wfl) as [Wl Af]; clear Wfl. rewrite length_map in Af. apply well_formed_fold; split. intros u u_in_l; apply (Hrec u u_in_l). apply Wl; rewrite in_map_iff; exists u; split. apply eq_refl. assumption. assumption. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)