proposition: Lemma eq_label_dec: forall p h s l l', (step_star (init p) h s /\ In l h /\ In l' h) -> (l = l') \/ (not (l = l')).
proof: Proof. intros. destruct H as [N1 [N2 N3]]. remember (init p) as s0 eqn: Hs. induction N1. inversion N2. depremise IHN1. assumption. assert (A := labels_step_unique p ls s2 l0 s3). depremise A. subst s1. split; assumption. apply in_app_iff in N2. apply in_app_iff in N3. destruct N2 as [N2 | N2]. destruct N3 as [N3 | N3]. apply IHN1. assumption. assumption. unfold In in N3. destruct N3 as [N3 | N3]; try contradiction. subst l0. right. intro. subst. contradiction. destruct N3 as [N3 | N3]. unfold In in N2. destruct N2 as [N2 | N2]; try contradiction. subst l0. right. intro. subst. contradiction. unfold In in N2. destruct N2 as [N2 | N2]; try contradiction. unfold In in N3. destruct N3 as [N3 | N3]; try contradiction. subst. left. reflexivity. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)