proposition: Lemma subst_comp_is_subst_comp_aux2 : forall v sigma1 sigma2, find (B:= term) eq_variable_dec v (sigma1 ++ sigma2) = match find eq_variable_dec v sigma1 with | Some _ => find eq_variable_dec v sigma1 | None => find eq_variable_dec v sigma2 end.
proof: Proof. intros v sigma1 sigma2; induction sigma1 as [ | [v1 a1] sigma1] ; trivial. simpl; elim (eq_variable_dec v v1); intro v_eq_v1; trivial. Qed.
imports: List more_list list_permut list_set Arith