proposition: Lemma move_valid s1 s2 : valid_state s1 -> move s1 s2 -> valid_state s2.
proof: Proof. intros Hg [H1 | [H1 | [H1 | [H1 | [H1 | [H1 | [H1 | [H1 | H1]]]]]]]]; subst s2; repeat (apply valid_state_right || apply valid_state_back || apply valid_state_down; auto). Qed.
imports: ZArith List