proposition: Lemma string_compare_eq : forall u v, string_compare u v = true -> u = v.
proof: Proof. intros u. induction u. intro v. induction v. intros. reflexivity. intros. discriminate. intros. induction v. discriminate. assert (bool_and (alphabet_compare t t0) (string_compare u v) =true). assumption. rewrite bool_and_true in H0. induction H0. rewrite (alphabet_compare_eq H0). rewrite (IHu _ H1). reflexivity. Qed.