proposition: Lemma cause_prefix_history_one: forall p h s l l' l'', (step_star (init p) (h ++ [l]) s /\ In l'' h /\ cause (h ++ [l]) l' l'') -> cause h l' l''.
proof: Proof. intros. open_conjs. assert (A: In l' h). eapply cause_in_pre_in. split_all; eassumption. eapply cause_in_prefix_history. split_all; eassumption. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)