proposition: Lemma has_first_char_nonempty str (H' : length str = 0) : get 0 str = None.
proof: Proof. case_eq (get 0 str); try reflexivity. intros ch H''. exfalso. apply get_0, length_singleton in H''. rewrite take_length, H' in H''. simpl in *; omega. 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