proposition: Lemma pb_check_level_fun_correct hiding P start_level : pb_check_level_fun hiding P start_level <-> (forall ch, P ch -> pb_check_level hiding ch start_level).
proof: Proof. unfold pb_check_level_fun. setoid_rewrite fold_right_andb_map_in_iff. setoid_rewrite filter_In. setoid_rewrite (fun x => @and_TrueP_L (In x (enumerate Char)) (P x = true) (enumerate_correct x)). reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Lists.List Coq.ZArith.ZArith Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BaseTypes Fiat.Common.List.Operations Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.Enumerable Fiat.Common.LogicFacts Fiat.Common.Equality