proposition: Lemma in_exec: forall (h: list Label)(s s': State)(l: Label), (step_star s h s' /\ In l h) -> exists (h1: list Label) (s1: State) (s2: State) (h2: list Label), (h = h1 ++ l :: h2 /\ step_star s h1 s1 /\ step s1 l s2 /\ step_star s2 h2 s').
proof: Proof. intros. destruct H as [H1 H2]. induction H1. inversion H2. apply in_app_or in H2. destruct H2. depremise IHstep_star. assumption. destruct IHstep_star as [h1 [s3' [s4' [h2 H2]]]]. open_conjs. exists h1. exists s3'. exists s4'. exists (h2 ++ [l0]). split_all; try assumption. subst ls. rewrite app_comm_cons. rewrite app_assoc. reflexivity. eapply steps; eassumption. clear IHstep_star. unfold In in H0. destruct H0; try contradiction. subst. exists ls. exists s2. exists s3. exists nil. split_all. reflexivity. assumption. assumption. constructor. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)