proposition: Lemma subst_comp_is_subst_comp_aux2 : forall v sigma1 sigma2, find (B:= term) eq_var_bool v (sigma1 ++ sigma2) = match find eq_var_bool v sigma1 with | Some _ => find eq_var_bool v sigma1 | None => find eq_var_bool v sigma2 end.
proof: Proof. fix subst_comp_is_subst_comp_aux2 2. intros v sigma1 sigma2; case sigma1; clear sigma1. reflexivity. intros p sigma; case p; clear p; intros v1 a1; simpl. case (eq_var_bool v v1). reflexivity. apply subst_comp_is_subst_comp_aux2. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)