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