This proves that instr_kinds are either the same or different.  As the
monotonicity proof is splitted in two case, one where two instrs are the
same, and one where two instrs are different, this will be useful to
reunite them.

Signed-off-by: Alban Gruin <alban.gruin@irit.fr>