proposition: Lemma fast_step_correct: forall task s l s', step_fun task s = Some (l, s') -> fast_step_fun task s = Some s'.
proof: Proof. Proof using max_nid_eq. unfold step_fun, fast_step_fun; intros. rewrite nids_eq in *. repeat match goal with | H: Some _ = Some _ |- _ => inversion H; clear H; subst | _ => rewrite nid_in_dec_existsb in * | H: (_ && _ = true)%bool |- _ => rewrite Bool.andb_true_iff in H; destruct H | H: (_ && _ = false)%bool |- _ => rewrite Bool.andb_false_iff in H; destruct H | H: None = Some _ |- _ => discriminate | _ => reflexivity | _ => mcase_eq in H | _ => mcase_eq | _ => congruence end. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)