proposition: Lemma cause_pre_cause: forall p h s l l' l'', (step_star (init p) (h++[l]) s /\ cause (h ++ [l]) l' l'' /\ (not (l = l''))) -> cause h l' l''.
proof: Proof. intros. destruct H as [H1 [H2 H3]]. assert (A1: In l'' h). apply cause_in in H2. destruct H2 as [_ H2]. apply in_app_iff in H2. destruct H2. assumption. simpl in H. destruct H; try contradiction. eapply cause_prefix_history_one. split_all. eassumption. assumption. assumption. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)