definition tape_move ≝ λsig.λt: tape sig.λm:sig × move.
match \snd m with
[ R ⇒ mk_tape sig ((\fst m)::(left ? t)) (tail ? (right ? t))
| L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m)::(right ? t))
| N ⇒ mk_tape sig (left ? t) ((\fst m)::(tail ? (right ? t)))
].
definition tape_move ≝ λsig.λt: tape sig.λm:sig × move.
match \snd m with
[ R ⇒ mk_tape sig ((\fst m)::(left ? t)) (tail ? (right ? t))
| L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m)::(right ? t))
| N ⇒ mk_tape sig (left ? t) ((\fst m)::(tail ? (right ? t)))
].