-[ % #t1 * #x * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
-|2,3: #a0 #al0 % #t1 * #x * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
-| #ls #c #rs lapply c -c lapply ls -ls lapply t -t elim rs
- [#t #ls #c % #t1 * #x * * >nth_change_vec // normalize in ⊢ (%→?);
- #H1 destruct (H1) #Hxsep >change_vec_change_vec #Ht1 %
- #t2 * #x0 * * >Ht1 >nth_change_vec_neq [|@sym_not_eq //]
+[ % #t1 * #x1 * #x2 * * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
+|2,3: #a0 #al0 % #t1 * #x1 * #x2 * * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
+| #ls lapply t -t elim ls
+ [#t #c #rs % #t1 * #x1 * #x2 * * * >nth_change_vec // normalize in ⊢ (%→?);
+ #H1 destruct (H1) #Hcurdst #Hxsep >change_vec_change_vec #Ht1 %
+ #t2 * #y1 * #y2 * * * >Ht1 >nth_change_vec_neq [|@sym_not_eq //]