proposition: Lemma lts_tail_unique a s1 s2 : lt (String a s1) (String a s2) -> lt s1 s2.
proof: Proof. intro H; inversion H; subst; auto. remember (nat_of_ascii a) as x. apply Nat.lt_irrefl in H1; inversion H1. Qed.
imports: OrderedType ZArith_base PeanoNat Peano_dec Compare_dec Ascii String NArith Ndec