Inference and Unification algorithm provided to a Unification graph of two expressions
Yes, your solution and process are correct, assuming that alpha and beta are variables. It might help to rewrite your terms in a more uniform way, e.g.

T1 = *(list(int), list(alpha))
T2 = *(alpha, beta)


Here, a term always satisfies the grammar:

Term ::= Constant
       | Variable
       | Func "(" Term+ ")"


Furthermore, it might clarify things to think of the unification process as taking a third argument: a substitution in which the two terms are to be unified. This substitution is simply an association between variables and terms, and it provides a context in which to resolve variables. Additionally, the unification process results in either a failure (if the terms do not unify in the substitution), or a substitution which both indicates success and provides a way to construct a "most general unifier".