proposition: Lemma tapp_x_nil_eq a u v: tapp u (tnil a) v -> a = ttail u /\ v = u.
proof: Proof. revert v; induction u. inversion_clear 1. now idtac. inversion_clear 1. edestruct IHu as (?&?). eassumption. subst. now idtac. Qed.
imports: prop monoid positives comparisons