proposition: Lemma override_eq: forall {V} n s (v1 v2: V), SysPredefs.override (SysPredefs.override s n v1) n v2 = SysPredefs.override s n v2.
proof: Proof. unfold SysPredefs.override; intros. apply functional_extensionality; intros. case_eq (x =_? n); intros; auto. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)