proposition: Lemma subst_rest_subst : forall vars sigma v t, In (v,t) (subst_rest vars sigma) -> In (v,t) sigma.
proof: Proof. fix subst_rest_subst 2. intros vars sigma; case sigma; clear sigma. intros v t; contradiction. intros p sigma; case p; clear p. intros z t v u; 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. intros [zt_eq_vu | vu_in_rest]. left; assumption. right; apply (subst_rest_subst vars); assumption. intros vu_in_rest; right; apply (subst_rest_subst vars); assumption. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)