proposition: Lemma forall_chars_singleton_length (str : String) P (H : length str = 1) : forall_chars str P <-> (forall ch, str ~= [ ch ] -> P ch).
proof: Proof. split. { intro H''. intros ch' H'''. apply (forall_chars_singleton _ _ _ H'''); assumption. } { destruct (singleton_exists _ H) as [ch H']. intro H''. apply (forall_chars_singleton _ P ch H'); eauto. } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Common