proposition: Lemma cause_prefix_history: forall p h h' s l l', (step_star (init p) (h ++ h') s /\ In l' h /\ cause (h ++ h') l l') -> cause h l l'.
proof: Proof. intros. open_conjs. generalize dependent s. induction h' using rev_ind. intros. rewrite app_nil_r in H1. assumption. intros. depremise IHh'. eapply cause_prefix_history_one. split_all. rewrite <- app_assoc. eassumption. apply in_app_iff. left. assumption. rewrite <- app_assoc. assumption. rewrite app_assoc in H. apply step_star_app in H. destruct H as [s2 [N1 N2]]. specialize (IHh' s2). depremise IHh'. assumption. assumption. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)