proposition: Lemma tapp_ass u v w uv uvw: tapp u v uv -> tapp uv w uvw -> exists vw, tapp v w vw /\ tapp u vw uvw.
proof: Proof. intro H. revert uvw. induction H. inversion_clear 1; eexists; split; constructor. inversion_clear 1. eexists; split; constructor; assumption. inversion_clear 1. edestruct IHtapp as (?&?&?). eassumption. eexists; split. eassumption. constructor. assumption. Qed.
imports: prop monoid positives comparisons