[STATEMENT]
lemma listI_assn_subst: 
  assumes "i\<notin>I "" i<length xs "
  shows "listI_assn (insert i I) A (xs[i:=x1]) (xsi[i := x2]) = A x1 x2 * listI_assn I A xs xsi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. listI_assn (insert i I) A (xs[i := x1]) (xsi[i := x2]) = A x1 x2 * listI_assn I A xs xsi
[PROOF STEP]
by (smt (z3) assms(1) assms(2) length_list_update listI_assn_def listI_assn_insert nth_list_update_eq pure_false star_false_left star_false_right subst_not_in)