proposition: Lemma tapp_cat u v: ttail u = thead v -> exists w, tapp u v w.
proof: Proof. induction u; simpl; intros Hu. rewrite Hu. eexists. apply tapp_nil_x. destruct IHu as [w ?]; trivial. eexists. constructor. eassumption. Qed.
imports: prop monoid positives comparisons