proposition: Lemma traces_deriv_dot_2 a i (H K: traces'): ~ (H (tnil a)) -> traces_deriv a i (H⋅K) ≡ traces_deriv a i H ⋅ K.
proof: Proof. intros Hnil w; simpl; unfold traces_deriv, traces_dot, pw2. split. intros [[b|b j u] Hu [v Kv E]]. apply tapp_nil_x_eq in E as [-> <-]. now elim Hnil. inversion E. subst. clear E. repeat eexists; eauto. intros [u Hu [v Kv E]]; repeat eexists; eauto using tapp_cons_x. Qed.
imports: prop monoid positives comparisons