proposition: Lemma label_node_in_nids: forall p h s l, (step_star (init p) h s /\ In l h) -> let n := label_node l in In n nids.
proof: Proof. intros. open_conjs. remember (init p) as s0 eqn: Hs. induction H. simpl in H0. contradiction. apply in_app_iff in H0. destruct H0. depremise IHstep_star. assumption. depremise IHstep_star. assumption. assumption. clear IHstep_star. simpl in H0. destruct H0; try contradiction. subst l0. inversion H1; subst n; subst l; simpl; assumption. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)