+ destruct (Htf) cut (tg = change_vec ?? ta (midtape ? ls (bit false) [c]) cfg)
+ [ @(eq_vec … (niltape ?)) #i #Hi cases (true_or_false (cfg == i)) #Hcfgi
+ [ <(\P Hcfgi) >nth_change_vec // @Htg1 //
+ | <(Htg2 ? (\Pf Hcfgi)) >(nth_change_vec_neq ??????? (\Pf Hcfgi))
+ >(nth_change_vec_neq ??????? (\Pf Hcfgi)) % ] ] -Htg1 -Htg2 #Htg
+ -Hth1 cut (th = change_vec ?? tg (midtape ? (bit false::ls) c []) cfg)
+ [ @(eq_vec … (niltape ?)) #i #Hi cases (true_or_false (cfg == i)) #Hcfgi
+ [ <(\P Hcfgi) >nth_change_vec // >Htg in Hth2; >nth_change_vec // #Hth2
+ @(Hth2 … (refl ??))
+ | <(Hth3 ? (\Pf Hcfgi)) >(nth_change_vec_neq ??????? (\Pf Hcfgi)) // ] ]
+ -Hth2 -Hth3 #Hth
+ cut (te = change_vec ?? th (midtape ? (bit false::ls) (bit false) [ ]) cfg)
+ [@daemon] -Hte1 -Hte2 #Hte
+ -Htj1 cut (tj = change_vec ?? te (midtape ? ls (bit false) [bit false]) cfg)
+ [@daemon] -Htj2 -Htj3 #Htj
+ -Htk1 cut (tk = change_vec ?? tj (mk_tape ? [ ] (None ?) (reverse ? ls@[bit false;bit false])) cfg)
+ [ @(eq_vec … (niltape ?)) #i #Hi cases (true_or_false (cfg == i)) #Hcfgi
+ [ <(\P Hcfgi) >nth_change_vec // >Htj in Htk2; >nth_change_vec // #Htk2
+ @(Htk2 … (refl ??))
+ | <(Htk3 ? (\Pf Hcfgi)) >(nth_change_vec_neq ??????? (\Pf Hcfgi)) // ] ]
+ -Htk2 -Htk3 #Htk >Htb >Htk >change_vec_change_vec >nth_change_vec //
+ >Htj >change_vec_change_vec >Hte >change_vec_change_vec
+ >Hth >change_vec_change_vec >Htg >change_vec_change_vec
+ >reverse_cons >reverse_cons
+
+
+ >nth_change_vec in Htg1; // #Htg1 lapply (Htg1 … (refl ??)) -Htg1 #Htg1
+ cut (∀j.cfg ≠ j → nth j ? ta (niltape ?) = nth j ? tg (niltape ?))
+ [ #j #Hj <Htg2 // >nth_change_vec_neq // ] -Htg2 #Htg2