proposition: Lemma subst_rest_ok : forall vars sigma v, In v vars -> apply_subst (subst_rest vars sigma) (Var v) = apply_subst sigma (Var v).
proof: Proof. fix subst_rest_ok 2. intros vars sigma; case sigma; clear sigma. intros v _; apply eq_refl. intros p sigma; case p; clear p. intros z t v v_in_vars; simpl. generalize (mem_bool_ok _ _ X.eq_bool_ok z vars); case (mem_bool eq_var_bool z vars); [intro z_in_vars | intro z_not_in_vars]. simpl. destruct (eq_var_bool v z). apply eq_refl. apply subst_rest_ok; trivial. generalize (X.eq_bool_ok v z); case (eq_var_bool v z); [intro v_eq_z | intro v_diff_z]. apply False_rect; apply z_not_in_vars; subst v; apply in_impl_mem. intros; apply eq_refl. assumption. apply subst_rest_ok; trivial. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)