proposition: Lemma split_exec: forall (h1 h2 h3: list Label)(s s': State)(l l': Label), step_star s (h1 ++ (l :: h2) ++ (l' :: h3)) s' -> exists s1 s2, (step_star s h1 s1 /\ step_star s1 (l :: h2 ++ [l']) s2 /\ step_star s2 h3 s').
proof: Proof. intros. apply step_star_app in H. destruct H as [s'' H]. destruct H as [H1 H2]. apply step_star_app in H2. destruct H2 as [s''' H2]. destruct H2 as [H2 H3]. apply step_star_end in H3. destruct H3 as [s'''' H3]. destruct H3 as [H3 H4]. exists s''. exists s''''. split. assumption. split. rewrite app_comm_cons. eapply steps; eassumption. assumption. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)