proposition: Lemma forall_chars_False (str : String) P : (forall ch, ~P ch) -> forall_chars str P -> length str = 0.
proof: Proof. intros H' H. case_eq (length str); trivial. specialize (H (length str - 1)). pose proof (singleton_exists (drop (length str - 1) str)) as H''. rewrite drop_length in H''. intros n H'''. rewrite H''' in *. rewrite sub_plus in H'' by omega. rewrite Nat.sub_diag in *. specialize (H'' eq_refl). destruct H'' as [ch H'']. exfalso; eapply H', H. rewrite take_long; try eassumption. apply length_singleton in H''; omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Common