proposition: Lemma labels_step_unique: forall p h s l s', (step_star (init p) h s /\ step s l s') -> not (In l h).
proof: Proof. intros. destruct H as [N1 N2]. intro. assert (L1 := label_num_steps p h s l). depremise L1. split; assumption. assert (L2 := label_num_inc s l s'). depremise L2. assumption. destruct L2 as [L2 L3]. assert (A: label_num l < label_num l). eapply Nat.le_lt_trans. apply L1. assumption. apply Nat.lt_irrefl in A. assumption. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)