Representation of proof s' by coloured graphs and Hadwiger hypothesis

Coloured graph is a directed graph with some vertices and ares coloured in some colours.
If $A$ is a set of $k$-vertex coloured graphs and $G$ is a coloured graph then $G$ is said to be $A$-well-coloured if all its $k$-vertex subgraphs belong to $A$.
We describe a construction of a finite set $B_p$ of 3-vertex graphs with ares coloured in some colours and a finite set $C_p$ of 2-vertex graphs with ares and vertices coloured in some colours for a given formula $P$ of the first order predicate calcules such that $\vdash P$ if and only if there exists $B_p$-well-(arc)coloured graph $G$ which does not permit $C_p$-well-colouring of vertices.
Hadwiger hypothesis (HH): if no subgraph of lopp-free graph $G$ is contracted to $n$-vertex complete graph, then vertices of $G$ can be coloured in $(n-1)$ colours in such a way that neighbouring vertices are coloured in distinct colours.
We construct a formula $X$ of the first order predicate calcules such that HH is equivalent to $\rceil\vdash X$. Thus HH is reduced to the statement.
If all 3-vertex subgraphs of arc-coloured graph $G$ belong to $B_X$ then the vertices of $G$ can be $C_X$-well-coloured.
Here $B_X$ and $C_X$ are concrete finite sets of 3-vertex and 2-vertex coloured graphs.