Rephrase Rechability to reuse ssreflect's lemmas.

Drawback: this makes the development depend on MathComp.
Admit the correctness of executable semantics w.r.t. declarative one.