proposition: Lemma subst_rest_subst_rest : forall vars sigma v t, In v vars -> In (v,t) sigma -> In (v,t) (subst_rest vars sigma).
proof: Proof. fix subst_rest_subst_rest 2; intros vars sigma; case sigma; clear sigma. intros; contradiction. intros p sigma; case p; clear p. simpl; intros x u v t x_in_vars. intros [xu_eq_vt | vt_in_sigma]. injection xu_eq_vt; clear xu_eq_vt; intros; subst v t. generalize (mem_bool_ok _ _ X.eq_bool_ok x vars); case (mem_bool X.eq_bool x vars); [intros _ | intro x_not_in_vars]. left; apply eq_refl. apply False_rect; apply x_not_in_vars; apply in_impl_mem; trivial. case (mem_bool X.eq_bool x vars). right; apply subst_rest_subst_rest; assumption. apply subst_rest_subst_rest; assumption. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)