proposition: Lemma take_of_string (n : nat) str : take n (of_string str) =s of_string (List.take n str).
proof: Proof. revert str; induction n; intros; simpl. { apply bool_eq_empty; rewrite ?take_length, ?drop_length; trivial. apply length_of_string_nil. } { apply bool_eq_from_get. intros_destruct. { destruct str as [|ch str]; simpl; repeat match goal with | _ => progress simpl | _ => reflexivity | _ => progress rewrite ?get_take_lt, ?get_of_string, ?take_length, ?length_of_string_nil by (reflexivity || omega) end. } { intro n'; rewrite !get_S. rewrite drop_take, !drop_of_string; simpl. rewrite Nat.sub_0_r. destruct str; simpl; rewrite !IHn; simpl; trivial. destruct n; reflexivity. } } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Common Fiat.Common.List.Operations Fiat.Common.List.ListFacts Fiat.Common.Le Fiat.Common.Tactics.SetoidSubst Fiat.Common.Tactics.IsClosed Fiat.Parsers.StringLike.Core Fiat.Common.UIP