proposition: Lemma well_formed_remove_term : forall sigma t, well_formed (apply_subst sigma t) -> forall x, var_in_term x t = true -> well_formed (apply_subst sigma (Var x)).
proof: Proof. intros sigma t; pattern t; apply term_rec3; clear t. intros v W x; simpl; generalize (X.eq_bool_ok v x); case (X.eq_bool v x). intros v_eq_x _; subst v; exact W. intros; discriminate. intros f l Hrec Wfl; simpl apply_subst in Wfl; destruct (well_formed_unfold Wfl) as [Wl _]; clear Wfl. intros v; rewrite var_in_term_is_sound; rewrite var_list_unfold. induction l as [ | t l]. contradiction. intros v_in_tl; destruct (in_app_or _ _ _ v_in_tl) as [v_in_t | v_in_l]. apply (Hrec t). left; reflexivity. apply Wl; rewrite in_map_iff; exists t; split. reflexivity. left; reflexivity. rewrite var_in_term_is_sound; assumption. apply IHl. apply (tail_prop _ Hrec). apply (tail_prop _ Wl). assumption. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)