proposition: Lemma state_eq_override: forall s n p u d r m, s n = node_state p u d r m -> s = SysPredefs.override s n (node_state p u d r m).
proof: Proof. Proof using. intros. apply functional_extensionality; intros. case_eq (n =? x); autorewrite with nat; intros; subst; simpl_override; auto. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)