- >Hsrc_tc in Hc0; normalize in ⊢ (%→?); #Hc0 destruct (Hc0)
-(* <(change_vec_same … tc src (niltape ?)) in Hd:(???(???(???%??)??));
- <(change_vec_same … tc dst (niltape ?)) in ⊢(???(???(???%??)??)→?); *)
- >Hdst_tc in Hd; >Hsrc_tc
-(* >change_vec_change_vec >change_vec_change_vec
- >(change_vec_commute ?? tc ?? dst src) [|@(sym_not_eq … Hneq)]
- >change_vec_change_vec *) @(list_cases2 … Hlen)
- [ #Hxsnil #Htargetnil >Hxsnil >Htargetnil #Hd >(IH2 … Hsep)
- [ >Hd -Hd @(eq_vec … (niltape ?))
- #i #Hi cases (decidable_eq_nat i src) #Hisrc
- [ >Hisrc >(nth_change_vec_neq … src dst) [|@(sym_not_eq … Hneq)]
- >nth_change_vec //
- >(nth_change_vec_neq … src dst) [|@(sym_not_eq … Hneq)]
- >nth_change_vec //
- | cases (decidable_eq_nat i dst) #Hidst
- [ >Hidst >nth_change_vec // >nth_change_vec //
- >Hdst_tc in Hc1; >Htargetnil
- normalize in ⊢ (%→?); #Hc1 destruct (Hc1) %
- | >nth_change_vec_neq [|@(sym_not_eq … Hidst)]
- >nth_change_vec_neq [|@(sym_not_eq … Hisrc)]
- >nth_change_vec_neq [|@(sym_not_eq … Hidst)]
- >nth_change_vec_neq [|@(sym_not_eq … Hisrc)] % ]
- ]
- | >Hd >nth_change_vec_neq [|@(sym_not_eq … Hneq)]
- >nth_change_vec // ]
+ >Hsrc_tc in Hc0; normalize in ⊢ (%→?); #Hc0 destruct (Hc0)
+ >Hdst_tc in Hd; >Hsrc_tc @(list_cases2 … Hlen)
+ [ #Hxsnil #Htargetnil >Hxsnil >Htargetnil #Hd >IH2
+ [2: %1 %1 %{sep} % // >Hd >nth_change_vec_neq [|@(sym_not_eq … Hneq)]
+ >nth_change_vec //]
+ >Hd -Hd @(eq_vec … (niltape ?))
+ #i #Hi cases (decidable_eq_nat i src) #Hisrc
+ [ >Hisrc >(nth_change_vec_neq … src dst) [|@(sym_not_eq … Hneq)]
+ >nth_change_vec //
+ | cases (decidable_eq_nat i dst) #Hidst
+ [ >Hidst >nth_change_vec //
+ | >nth_change_vec_neq [|@(sym_not_eq … Hidst)]
+ >nth_change_vec_neq [|@(sym_not_eq … Hisrc)] %
+ ]
+ ]