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