proposition: Lemma valid_nid_step_fun_Proc: forall n1 s l s', step_fun (SchedProc n1) s = Some (l, s') -> List.In n1 nids.
proof: Proof. Proof using. simpl; intros. rewrite nid_in_dec_existsb in *. mcase_eq in H; auto. discriminate. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)