proposition: Theorem append_correct1 : forall (s1 s2 : string) (n : nat), n < length s1 -> get n s1 = get n (s1 ++ s2).
proof: Proof. intros s1; elim s1; simpl; auto. - intros s2 n H; inversion H. - intros a s1' Rec s2 n; case n; simpl; auto. intros n0 H; apply Rec; auto. apply Nat.succ_lt_mono; auto. Qed.
imports: Arith Ascii Bool Coq.Strings.Byte