proposition: Lemma cause_in_prefix_history: forall p h l'' s l l', (step_star (init p) (h ++ [l'']) s /\ In l h /\ In l' h /\ cause (h ++ [l'']) l l') -> cause h l l'.
proof: Proof. intros. open_conjs. remember (h ++ [l'']) as he eqn: Hh. induction H2. subst h0. apply cause_cause_step. eapply cause_step_in_prefix_history. split_all; eassumption. subst h0. assert (A: In l' h). eapply cause_in_pre_in. split_all. eassumption. apply H1. constructor. assumption. depremise IHcause. reflexivity. depremise IHcause. assumption. depremise IHcause. assumption. depremise IHcause. assumption. eapply cause_trans. eassumption. eapply cause_step_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)