proposition: Lemma move_eqb_spec x y : reflect (x = y) (move_eqb x y).
proof: Proof. destruct x, y;constructor. all:easy. Qed.
imports: Undecidability.L.Datatypes(LVector) Undecidability.L(Functions.EqBool) Undecidability.TM.Util(TM_facts) Undecidability.L.Tactics(LTactics GenEncode)