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.
Proof by contradiction is easy in this case.

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.