fact: Definition forall_chars__impl__forall_chars__char_in {str ls} {P : _ -> Prop} (H : forall ch, P ch -> List.In ch ls) : impl (forall_chars str P) (forall_chars__char_in str ls).
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Common