proposition: Lemma update_update_neq : forall l i j v w, index l i -> index l j -> i <> j -> l[i:=v][j:=w] = l[j:=w][i:=v].
proof: Proof. Proof using. intros. asserts IA: (Inhab A). typeclass. applys eq_of_extens; repeat rewrite length_update. { auto. } intros k Hk. repeat rewrite index_update_eq in Hk. repeat rewrite read_update_case by eauto using index_update. repeat case_if~. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)