proposition: Lemma cause_step_in: forall h l l', cause_step h l l' -> (In l h /\ In l' h).
proof: Proof. intros. unfold cause_step in H; destruct H; open_conjs; unfold prec in H; destruct H as [h1 [h2 [h3 H]]]; rewrite H; split; apply in_app_iff; right. apply in_eq; apply in_app_iff; right; apply in_app_iff; right; apply in_eq. apply in_app_iff. right. apply in_eq. apply in_eq. apply in_app_iff. right. apply in_eq. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)