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