proposition: Lemma cause_prec: forall p h s l l', (step_star (init p) h s /\ cause h l l') -> prec h l l'.
proof: Proof. intros. open_conjs. induction H0. unfold cause_step in H0. destruct H0; open_conjs; assumption. assert (A: prec h l' l''). unfold cause_step in H1. destruct H1; open_conjs; assumption. depremise IHcause. assumption. eapply prec_trans; eauto. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)