proposition: Theorem index_inj : forall (x y : t), index x = index y -> x = y.
proof: Proof. induction x; destruct y; intros. - reflexivity. - simpl in *. unfold list_bool_of_ascii in *. break_let; simpl in * ; repeat break_match; congruence. - simpl in *. unfold list_bool_of_ascii in *. break_let; simpl in *; repeat break_match; congruence. - simpl in *. unfold list_bool_of_ascii in *. repeat break_let. find_apply_lem_hyp positive_of_digits_inj. + subst. break_and. find_inversion. find_apply_hyp_hyp. subst. reflexivity. + reflexivity. Qed.
imports: Coq(ZArith) Coq(FMapInterface FMapPositive) Coq(FMapList FMapFacts) Coq(String Ascii List) StructTact(StructTactics StringOrders)