proposition: Lemma cause_pre_in: forall p h l s l', (step_star (init p) (h ++ [l]) s /\ cause (h ++ [l]) l' l) -> In l' h.
proof: Proof. intros. destruct H as [N1 N2]. assert (A1: prec (h ++ [l]) l' l). eapply cause_prec. split; eassumption. unfold prec in A1. destruct A1 as [h1 [h2 [h3 A1]]]. assert (A2: l :: h3 <> nil). intro. inversion H. assert (L := exists_last A2). destruct L. destruct s0. rewrite e in A1. clear A2 e. rewrite app_assoc in A1. rewrite app_assoc in A1. apply app_inj_tail in A1. destruct A1 as [A1 A2]. rewrite A1. apply in_app_iff. left. apply in_app_iff. right. apply in_eq. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)