proposition: Lemma label_num_steps_lower: forall h s s' l, step_star s h s' -> In l h -> latest_label s < label_num l.
proof: Proof. induction 1; t; eauto using Nat.le_trans, Nat.lt_le_trans. apply in_app_or in H1; intuition eauto. simpl in *; intuition subst. apply label_num_inc in H0; intuition. apply step_star_latest_label in H. lia. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)