- >change_vec_change_vec
- >(change_vec_commute … ?? td ?? dst src) [|@sym_not_eq //]
- >change_vec_change_vec
- >reverse_cons >associative_append
- >reverse_cons >associative_append %
- | >Hd >nth_change_vec //
- | >Hxs in Hlen; >Htarget normalize #Hlen destruct (Hlen) //
- | >Hd >nth_change_vec_neq [|@sym_not_eq //]
- >nth_change_vec // ]
- ]
- | >Hc0 >Hc1 * [ #Hc0 destruct (Hc0) | #Hc1 destruct (Hc1) ]
- ] ]
+ >change_vec_change_vec
+ >(change_vec_commute … ?? td ?? dst src) [|@sym_not_eq //]
+ >change_vec_change_vec
+ >reverse_cons >associative_append
+ >reverse_cons >associative_append %
+ | >Hd >nth_change_vec //
+ | >Hxs in Hlen; >Htarget normalize #Hlen destruct (Hlen) //
+ | >Hd >nth_change_vec_neq [|@sym_not_eq //]
+ >nth_change_vec // ]
+ ]
+ | #x #xs #rs #Hdst_td #ls0 #x0 #target
+ #rs0 #Hlen #Hsrc_td
+ >Hdst_td in Hc0; normalize in ⊢ (%→?); #Hc0 destruct (Hc0)
+ >Hsrc_td in Hd; >Hdst_td @(list_cases2 … Hlen)
+ [ #Hxsnil #Htargetnil >Hxsnil >Htargetnil #Hd >IH2
+ [2: %2 >Hd >nth_change_vec //]
+ >Hd -Hd @(eq_vec … (niltape ?))
+ #i #Hi cases (decidable_eq_nat i dst) #Hidst
+ [ >Hidst >(nth_change_vec_neq … dst src) //
+ >nth_change_vec // >nth_change_vec //
+ | cases (decidable_eq_nat i src) #Hisrc
+ [ >Hisrc >nth_change_vec // >(nth_change_vec_neq …) [|@sym_not_eq //]
+ >Hsrc_td in Hc1; >Htargetnil
+ normalize in ⊢ (%→?); #Hc1 destruct (Hc1) >nth_change_vec //
+ cases ls0 //
+ | >nth_change_vec_neq [|@(sym_not_eq … Hidst)]
+ >nth_change_vec_neq [|@(sym_not_eq … Hisrc)]
+ >nth_change_vec_neq [|@(sym_not_eq … Hisrc)]
+ >nth_change_vec_neq [|@(sym_not_eq … Hidst)] %
+ ]
+ ]
+ | #hd1 #hd2 #tl1 #tl2 #Hxs #Htarget >Hxs >Htarget #Hd
+ >(IH1b hd1 tl1 (x::rs) ? ls0 hd2 tl2 (x0::rs0))
+ [ >Hd >(change_vec_commute … ?? td ?? dst src) [|@sym_not_eq //]
+ >change_vec_change_vec
+ >(change_vec_commute … ?? td ?? src dst) //
+ >change_vec_change_vec
+ >reverse_cons >associative_append
+ >reverse_cons >associative_append
+ >change_vec_commute [|@sym_not_eq //] %
+ | >Hd >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec //
+ | >Hxs in Hlen; >Htarget normalize #Hlen destruct (Hlen) //
+ | >Hd >nth_change_vec // ]
+ ]
+ ]
+| >Hc0 >Hc1 * [ #Hc0 destruct (Hc0) | #Hc1 destruct (Hc1) ]
+] ]