proposition: Theorem get_correct : forall s1 s2 : string, (forall n : nat, get n s1 = get n s2) <-> s1 = s2.
proof: Proof. intros s1; elim s1; simpl. - intros s2; case s2; simpl; split; auto. + intros H; generalize (H O); intros H1; inversion H1. + intros; discriminate. - intros a s1' Rec s2; case s2 as [|? s]; simpl; split; auto. + intros H; generalize (H O); intros H1; inversion H1. + intros; discriminate. + intros H; generalize (H O); simpl; intros H1; inversion H1. case (Rec s). intros H0; rewrite H0; auto. intros n; exact (H (S n)). + intros [= H1 H2]. rewrite H2; trivial. rewrite H1; auto. Qed.
imports: Arith Ascii Bool Coq.Strings.Byte