proposition: Lemma move_Movel s s1 : move s s1 -> exists a, In a Movel /\ s1 = m2f a s.
proof: Proof. intros [H1|[H1|[H1|[H1|[H1|[H1|[H1|[H1|H1]]]]]]]]; subst. - exists Right; simpl; split; auto. - exists Right2; simpl; split; auto. - exists Rightm1; simpl; split; auto. - exists Back; simpl; split; auto. - exists Back2; simpl; split; auto; right; auto. - exists Backm1; simpl; split; auto; do 2 right; auto. - exists Down; simpl; split; auto; do 3 right; auto. - exists Down2; simpl; split; auto; do 4 right; auto. - exists Downm1; simpl; split; auto; do 5 right; auto. Qed.
imports: ZArith List