+qed.
+
+(* NO GOOD: we must stop if current = None too!!!
+lemma ssem_move_char_l :
+ ∀alpha,sep.
+ Realize alpha (move_char_l alpha sep) (R_move_char_l alpha sep).
+#alpha #sep *
+[ %{5} % [| % [whd in ⊢ (??%?);
+ @WRealize_to_Realize // @terminate_move_char_l
+*)
+
+axiom ssem_move_char_l :
+ ∀alpha,sep.
+ Realize alpha (move_char_l alpha sep) (R_move_char_l alpha sep).