- [#_ whd in Htrue; >Hmidta_src in Htrue; #Htrue
- cases (Htrue ?? (refl ??)) -Htrue >Hcurta_dst
- (* dovremmo sapere che ta.dst è sul margine destro, da cui la move non
- ha effetto *) #_ cut (tc = ta) [@daemon] #Htc destruct (Htc) #_
+ [#Hcurta_dst #Hrightta_dst whd in Htrue; >Hmidta_src in Htrue; #Htrue
+ cases (Htrue ?? (refl ??)) -Htrue #Htc
+ cut (tc = ta)
+ [ >Htc whd in match (tape_move_mono ???); whd in match (tape_write ???);
+ <(change_vec_same … ta dst (niltape ?)) in ⊢ (???%);
+ lapply Hrightta_dst lapply Hcurta_dst -Hrightta_dst -Hcurta_dst
+ cases (nth dst ? ta (niltape ?))
+ [ #_ #_ %
+ | #r0 #rs0 #_ normalize in ⊢ (%→?); #H destruct (H)
+ | #l0 #ls0 #_ #_ %
+ | #ls #x0 #rs normalize in ⊢ (%→?); #H destruct (H) ] ]
+ -Htc #Htc destruct (Htc) #_