+definition map_move ≝
+ λc,mv.match c with [ null ⇒ None ? | _ ⇒ Some ? 〈c,false,move_of_unialpha mv〉 ].
+
+definition current_of_alpha ≝ λc:STape.
+ match \fst c with [ null ⇒ None ? | _ ⇒ Some ? c ].
+
+definition legal_tape ≝ λls,c,rs.
+ let t ≝ mk_tape STape ls (current_of_alpha c) rs in
+ left ? t = ls ∧ right ? t = rs ∧ current ? t = current_of_alpha c.
+
+lemma legal_tape_cases :
+ ∀ls,c,rs.legal_tape ls c rs →
+ \fst c ≠ null ∨ (\fst c = null ∧ ls = []) ∨ (\fst c = null ∧ rs = []).
+#ls #c #rs cases c #c0 #bc0 cases c0
+[ #c1 normalize #_ % % % #Hfalse destruct (Hfalse)
+| cases ls
+ [ #_ % %2 % %
+ | #l0 #ls0 cases rs
+ [ #_ %2 % %
+ | #r0 #rs0 normalize * * #Hls #Hrs destruct (Hrs) ]
+ ]
+|*: #_ % % % #Hfalse destruct (Hfalse) ]
+qed.
+