proposition: Lemma traces_deriv_itr a i (H: traces'): traces_deriv a i (H^+) ≡ traces_deriv a i H ⋅ H^*.
proof: Proof. rewrite str_itr. apply antisym. - intro w. intros [n Hn]. induction n in a, i, w, Hn; simpl in Hn. repeat eexists; eauto. 2: apply tapp_x_nil. now left. destruct Hn as [[b|b j v] Hv [u Hu Hw]]. apply tapp_nil_x_eq in Hw as [-> <-]. apply IHn, Hu. inversion Hw. subst. clear Hw. repeat eexists; eauto. right. eexists; eauto. - intros w [u Hu [v [Hv|[n Hv]] Hw]]. destruct v as [b|]. 2: elim Hv. apply tapp_x_nil_eq in Hw as [-> <-]. now exists O. exists (S n). repeat eexists; eauto using tapp_cons_x. Qed.
imports: prop monoid positives comparisons