+
+lemma terminate_move_char_l :
+ ∀alpha,sep.∀t,b,a,ls,rs. t = midtape alpha ls b (a::rs) →
+ (b = sep ∨ memb ? sep ls = true) → Terminate alpha (move_char_l alpha sep) t.
+#alpha #sep #t #b #a #ls #rs #Ht #Hsep
+@(terminate_while … (sem_mcl_step alpha sep))
+ [%
+ |generalize in match Hsep; -Hsep
+ generalize in match Ht; -Ht
+ generalize in match rs; -rs
+ generalize in match a; -a
+ generalize in match b; -b
+ generalize in match t; -t
+ elim ls
+ [#t #b #a #rs #Ht #Hsep % #tinit
+ whd in ⊢ (%→?); #H @False_ind
+ cases (H … Ht) #Hb #_ cases Hb #eqb @eqb
+ cases Hsep // whd in ⊢ ((??%?)→?); #abs destruct
+ |#l0 #ls0 #Hind #t #b #a #rs #Ht #Hsep % #tinit
+ whd in ⊢ (%→?); #H
+ cases (H … Ht) #Hbsep #Htinit
+ @(Hind … Htinit) cases Hsep
+ [#Hb @False_ind /2/ | #Hmemb cases (orb_true_l … Hmemb)
+ [#eqsep %1 >(\P eqsep) // | #H %2 //]
+ ]
+qed.
\ No newline at end of file