proposition: Lemma movel_valid f s : In f movel -> valid_state s -> valid_state (f s).
proof: Proof. intros [H1 | [H1 | [H1 | [H1 | [H1 | [H1 | [H1 | [H1 | [H1 | H1]]]]]]]]]; try subst f; intros; repeat apply valid_state_right; repeat apply valid_state_back; repeat apply valid_state_down; auto. case H1; auto. Qed.
imports: ZArith List