- | #tmp2 #l3 normalize #H1 destruct (H1) ]
- ]
- | #r1 #rs1 normalize in ⊢ (???(????%?)→?); #Htb >Htb in IH; #IH
- cases (IH ls x xs end rs ? Hnotend Hend Hnotstart)
- [| >Htb >nth_change_vec_neq [|@sym_not_eq //] @Hmid_src ] -IH
- #_ #IH cases (IH Hstart (c::ls0) r1 rs1 ?)
- [|| >nth_change_vec // ] -IH
- [ * #l * #l1 * #Hll1 #Hout % %{(c::l)} %{l1} % >Hll1 //
- >reverse_cons >associative_append #cj0 #ls #Hl1 >(Hout ?? Hl1)
- >change_vec_commute in ⊢ (??(???%??)?); // @sym_not_eq //
- | #IH %2 @(not_sub_list_merge_2 ?? (x::xs)) normalize [|@IH]
- #l1 % #H destruct (H) cases eqx /2/
- ] *)
+ | #tmp2 #l3 normalize #H1 destruct (H1) ] ]
+ | #r1 #rs1 #_ #IH cases (IH … (refl ??)) -IH
+ [ * #l * #l1 * #Hll1 #Houtc % %{(c::l)} %{l1} % [ >Hll1 % ]
+ >Houtc >change_vec_commute // >change_vec_change_vec
+ >change_vec_commute [|@sym_not_eq //]
+ >reverse_cons >associative_append %
+ | #Hll1 %2 @(not_sub_list_merge_2 ?? (x::xs)) normalize [|@Hll1]
+ #l1 % #H destruct (H) cases (\Pf eqx) /2/
+ ]
+ ]