- | >Hd >nth_change_vec // >nth_change_vec_neq [|@sym_not_eq //]
- >nth_change_vec // >Hnthi >Hnthj normalize
- cases Hcicj #Hcase
- [%1 %{ci} % // | %2 %1 %1 @(not_to_not ??? Hcase) #H destruct (H) % ]
- ]
- | #x0 #xs0 #Hnthi #Hnthj #Hnotendc #Hcicj
- >(IH2 (c0::ls) x0 xs0 ci rs (c0::ls0) cj rs0 … Hcicj)
- [ >Hd >change_vec_commute in ⊢ (??%?); //
- >change_vec_change_vec >change_vec_commute in ⊢ (??%?); //
+ | >Hd %2 % % >nth_change_vec //
+ >nth_change_vec_neq [|@sym_not_eq //]
+ >nth_change_vec // >Hnthi >Hnthj normalize @(not_to_not … Hcir1)
+ #H destruct (H) % ]
+ ]
+ ]
+ |#x0 #xs0 #Hnthi #Hnthj #Hnotendc
+ cut (c0 = x) [ >Hnthi in Hci; normalize #H destruct (H) // ]
+ #Hcut destruct (Hcut) cases rs0 in Hnthj;
+ [ #Hnthj % % //
+ cases (IH2 (x::ls) x0 xs0 ci rs (x::ls0) [ ] ???) -IH2
+ [ * #_ #IH2 >IH2 >Hd >change_vec_commute in ⊢ (??%?); //
+ >change_vec_change_vec >change_vec_commute in ⊢ (??%?); //
+ @sym_not_eq //
+ | * #cj * #rs1 * #H destruct (H)
+ | >Hd >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec //
+ >Hnthi %
+ | >Hd >nth_change_vec // >Hnthj %
+ | #c0 #Hc0 @Hnotendc @memb_cons @Hc0 ]
+ | #r1 #rs1 #Hnthj %2 %{r1} %{rs1} % // #Hcir1
+ cases(IH2 (x::ls) x0 xs0 ci rs (x::ls0) (r1::rs1) ???)
+ [ * #H destruct (H)
+ | * #r1' * #rs1' * #H destruct (H) #Hc1r1 >Hc1r1 //
+ >Hd >change_vec_commute in ⊢ (??%?); //
+ >change_vec_change_vec >change_vec_commute in ⊢ (??%?); //