proposition: Lemma nids_eq: nids = SysPredefs.nids.
proof: Proof. Proof using max_nid_eq. unfold nids, SysPredefs.nids; intros; rewrite max_nid_eq; reflexivity. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)