proposition: Lemma move_sym s1 s2 : valid_state s1 -> move s1 s2 -> move s2 s1.
proof: Proof. intros Hg [H1 | [H1 | [H1 | [H1 | [H1 | [H1 | [H1 | [H1 | H1]]]]]]]]; subst s2; try (pattern s1 at 2; rewrite <- right_4; unfold move; auto; fail); try (pattern s1 at 2; rewrite <- down_4; auto; unfold move; do 6 right; auto; fail); pattern s1 at 2; rewrite <- back_4; auto; unfold move; do 3 right; auto. Qed.
imports: ZArith List