proposition: Lemma string_compare_refl : forall u, string_compare u u = true.
proof: Proof. intro u. induction u. reflexivity. change (bool_and (alphabet_compare t t) (string_compare u u) = true). rewrite alphabet_compare_refl. assumption. Qed.