proposition: Lemma Forall_update : forall P l i x, Forall P l -> P x -> index l i -> Forall P (l[i:=x]).
proof: Proof. Proof using. introv. gen i. induction l; introv HL Hx Hi; rew_listx. { rew_index in Hi. rew_list in *. false. math. } { rew_index in *. rew_listx* in HL. destruct HL. rewrite* update_cons_case. case_if*; rew_listx*. } Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)