+ |#b #Hcurrent @(list_of_tape_write ? is_bit … (char_to_bit_option c) ? Honlybits)
+ [#b0 cases c
+ [#b1 whd in ⊢ (??%?→?); #Hbit destruct (Hbit) %
+ |whd in ⊢ (??%?→?); #Hbit destruct (Hbit)
+ |whd in ⊢ (??%?→?); #Hbit destruct (Hbit)
+ ]
+ |>(list_of_tape_move … (char_to_move m)) @current_in_list @Hcurrent
+ ]
+ ]
+qed.