+(*
+lemma step_eq : ∀sig,M,c.
+ let current_char ≝ current ? (ctape ?? c) in
+ let 〈news,a,mv〉 ≝ trans sig M 〈cstate ?? c,current_char〉 in
+ step sig M c =
+ mk_config ?? news (tape_move sig (tape_write ? (ctape ?? c) a) mv).
+#sig #M #c
+ whd in match (tape_move_mono sig ??);
+*)
+