proposition: Lemma label_num_steps: forall p h s l, (step_star (init p) h s /\ In l h) -> (label_num l <= latest_label s).
proof: Proof. intros. destruct H as [N1 N2]. remember (init p) as s0 eqn: E. induction N1. unfold In in N2. contradiction. depremise IHN1. assumption. apply in_app_iff in N2. destruct N2 as [N2 | N2]. depremise IHN1. assumption. subst s1. assert (A := label_num_inc s2 l0 s3). depremise A. assumption. destruct A. apply Nat.lt_le_incl. eapply Nat.le_lt_trans. eassumption. eapply Nat.lt_le_trans; eassumption. simpl in N2. destruct N2; try contradiction. subst l0. clear N1 IHN1. assert (A:= label_num_inc s2 l s3 H). destruct A. assumption. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)