proposition: Lemma cause_in_pre_in: forall p h l'' s l l', (step_star (init p) (h ++ [l'']) s /\ In l' h /\ cause (h ++ [l'']) l l') -> In l h.
proof: Proof. intros. open_conjs. assert (L := cause_prec p (h++[l'']) s l l'). depremise L. split; assumption. unfold prec in L. destruct L as [h1 [h2 [h3 L]]]. apply in_split in H0. destruct H0 as [h1' [h2' H0]]. rewrite H0 in L. destruct h3. rewrite app_assoc in L. apply app_inj_tail in L. open_conjs. rewrite H0. rewrite H2. apply in_app_iff. right. apply in_eq. assert (A: l0 :: h3 <> nil). intro. inversion H2. assert (M := exists_last A). destruct M. destruct s0. rewrite e in L. clear A e. rewrite app_comm_cons in L. rewrite app_assoc in L. rewrite app_assoc in L. apply app_inj_tail in L. open_conjs. rewrite H0. rewrite H2. 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)