+The following machine implements a full move for a trace: we reach the left
+border, shift the i-th trace and come back to the head position.
+The head may hold additional information A, so we suppose that the tape alphabet
+is the disjoint sum between A and the alphabet sig of the multi tape machine. *)
+
+definition TA ≝ λA,sig. FinSum A sig.
+definition MTA ≝ λA,sig,n.multi_sig (TA A sig) n.
+
+definition is_head ≝ λA,sig.λc:sig_ext (TA A sig).
+ match c with
+ [ None ⇒ false
+ | Some a ⇒ match a with
+ [ inl _ ⇒ true
+ | inr _ ⇒ false]].
+
+definition is_sig ≝ λA,sig.λc:sig_ext (TA A sig).
+ match c with
+ [ None ⇒ false
+ | Some a ⇒ match a with
+ [ inl _ ⇒ false
+ | inr _ ⇒ true]].
+
+definition not_head ≝ λA,sig,n.λc:multi_sig (TA A sig) (S n).
+ ¬(is_head A sig (nth n ? (vec … c) (blank ?))).
+
+lemma not_head_all_blanks : ∀A,sig,n.
+ not_head A sig n (all_blanks … (S n)) = true.
+#A #sig #n whd in ⊢ (??%?); >blank_all_blanks //
+qed.
+
+definition no_head_in ≝ λA,sig,n,l.
+ ∀x. mem ? x (trace (TA A sig) (S n) n l) → is_head … x = false.
+
+(*
+lemma not_head_true: ∀A,sig,n,c. not_head A sig n c = true →
+ is_head … (nth n ? (vec … c) (blank ?)) = false.
+*)