proposition: Lemma prec_in_prefix_history: forall p h h' s l l', step_star (init p) (h ++ h') s -> In l' h -> prec (h ++ h') l l' -> prec h l l'.
proof: Proof. unfold prec; firstorder. eapply step_star_NoDup in H. destruct H; simpl in *. autorewrite with core in *. apply NoDup_app_bwd in H; intuition. rewrite app_comm_cons in H1. rewrite app_assoc in H1. eapply force_split in H1. - firstorder subst. rewrite <- app_assoc. simpl; eauto. - intro. eapply H5. eapply in_map_iff; eauto. apply in_map_iff. eauto. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)