# How to formally prove that a given hash construction is collision resistant or not?

Is there a precise procedure or strategy to follow in order to prove in a formal way the (not) collision-resistance of a certain given hash construction? I.e. let $H_1$ and $H_2$ be two hash functions, then define the following construction $H(x) = H_1(x)||H_2(x)$. How could one formally prove that such construction does not yield any collision, given that at least one of $H_1$ and $H_2$ is collision resistant?
I know, in this case, the concatenation of a sequence of hash functions is collision resistant if at least one of the hash functions in the sequence is collision resistant. But, my question here is if there's any formal way of proving it.

Assume the construction is not collision resistant. Then there's an adversary who can efficiently find a pair $H(x) = H(x')$. However, that also gives them $H_1(x) = H_1(x')$ and $H_2(x) = H_2(x')$, so neither hash function is collision resistant, which contradicts the assumption.
I think I found the answer to my own question, and please correct me if I'm wrong. Just for example, let $H_1$ be the collision resistant hash function and $H_2$ the not collision resistant one. This means that for some certain input $x' \neq x$, $H_2(x')=H_2(x)$. So $H(x) = H_1(x)||H_2(x)=h_1||h_2$ and $H(x') = H_1(x')||H_2(x')=h_1'||h_2$, which means that $H(x) \neq H(x')$ because $h_1 \neq h_1'$.