proposition: Lemma labels_unique: forall p h s l l', (step_star (init p) h s /\ prec h l l') -> not (l = l').
proof: Proof. intros. intro. open_conjs. subst l'. assert (A := prec_exec p h s l l). depremise A. split. assumption. assumption. destruct A as [h1 [s1 [s1' [h2 [s2' [s2 [h3 A]]]]]]]. open_conjs. assert (L := labels_step_unique p (h1++l::h2) s2' l s2). depremise L. split. apply step_star_app. exists s1. split. assumption. apply step_star_end. exists s1'. split; assumption. assumption. unfold not in L. apply L. apply in_app_iff. right. apply in_eq. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)