proposition: Lemma prec_pre_in: forall p h s l l', (step_star (init p) (h ++ [l]) s /\ prec (h ++ [l]) l' l) -> In l' h.
proof: Proof. unfold prec; firstorder. apply prec_split in H0; firstorder (subst; eauto using in_eq, in_or_app). Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)