proposition: Lemma Eq_eq : forall x y, string_compare x y = Eq -> x = y.
proof: Proof. induction x; destruct y; simpl; first [ discriminate | intros; f_equal; destruct_comparisons; autorewrite_nat_compare; rewrite nat_of_ascii_injective in * | idtac ]; intuition. Qed.
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Strings.Ascii Coq.Structures.OrderedType Fiat.Common.Coq__8_4__8_5__Compat