proposition: Lemma prec_pre_post_in: forall p h h' s l l', (step_star (init p) (h++ [l'] ++h') s /\ prec (h ++ [l'] ++ h') l l') -> In l h.
proof: Proof. intros. open_conjs. rewrite app_assoc in H. generalize H; intro Hdup. eapply prec_in_prefix_history in Hdup. 2: apply in_or_app; simpl; eauto. 2: rewrite <- app_assoc; eauto. eapply step_star_NoDup in H. destruct H. clear H0. unfold prec in Hdup; firstorder subst. rewrite <- (app_nil_r (h ++ [l'])) in H0. rewrite <- app_assoc in H0. rewrite (app_assoc x) in H0. autorewrite with core in H. apply NoDup_app_bwd in H; intuition. eapply NoDup_map_middle in H0. 2: autorewrite with core; eauto. 2: auto. intuition subst. apply in_or_app; simpl; eauto. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)