proposition: Lemma step_label_check_no_fault'': forall task s l s' n, step_fun task s = Some (l, s') -> check_no_fault'' nids s = true -> l <> fault_label n.
proof: Proof. Proof using. unfold step_fun, check_no_fault''; intros. clear max_nid_eq. repeat ( mcase_eq in H; repeat match goal with | H: Some _ = Some _ |- _ => inversion H; clear H; subst | _ => rewrite nid_in_dec_existsb in * | _ => discriminate end). rewrite List.forallb_forall in H0. specialize (H0 n0 i). rewrite H3 in H0. simpl in H0. discriminate. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)