proposition: Lemma Movel_move s a : In a Movel -> move s (m2f a s).
proof: Proof. simpl; intros [H1|[H1|[H1|[H1|[H1|[H1|[H1|[H1|[H1|H1]]]]]]]]]; subst; simpl; red; auto; do 3 right; auto; do 3 right; auto. case H1. Qed.
imports: ZArith List