proposition: Lemma label_num_inc: forall s l s', step s l s' -> (latest_label s < label_num l /\ label_num l <= latest_label s').
proof: Proof. intros. inversion H; simpl; split; try apply Nat.le_refl; try apply Nat.lt_succ_diag_r. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)