proposition: Lemma pb_new_level_fun_correct P start_level new_level : pb_new_level_fun P start_level = [new_level] <-> ((exists ch, P ch) /\ forall ch, P ch -> new_level = pb_new_level ch start_level).
proof: Proof. unfold pb_new_level_fun. rewrite (uniquize_singleton (beq := Nat.eqb) bl lb). setoid_rewrite in_map_iff. setoid_rewrite filter_In. setoid_rewrite (fun x => @and_TrueP_L (In x (enumerate Char)) (P x = true) (enumerate_correct _)). split; intro H; repeat match goal with | _ => split | _ => intro | _ => progress subst | _ => progress destruct_head ex | _ => progress split_and | _ => progress split_iff | [ H : forall x, _ = x -> _ |- _ ] => specialize (H _ eq_refl) | [ H : forall x, x = _ -> _ |- _ ] => specialize (H _ eq_refl) | [ H : forall x, _ -> _ = _ |- _ ] => unique pose proof (fun x H' => eq_sym (H x H')) | _ => solve [ eauto ] end. 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