proposition: Lemma forallb_forall_false : forall (A : Type) (f : A -> bool) (l : list A), forallb f l = false <-> ~ (forall x : A, In x l -> f x = true).
proof: Proof. setoid_rewrite <- forallb_forall. intros; destruct (forallb f l); split; congruence. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.ADT.Core Bedrock.Platform.Facade.DFModule Fiat.ADTNotation Bedrock.Platform.Facade.CompileUnit2 Fiat.Common.i3list Fiat.Common.ilist3 CertifiedExtraction.Core CertifiedExtraction.FacadeUtils CertifiedExtraction.StringMapUtils CertifiedExtraction.Extraction.Internal CertifiedExtraction.Extraction.Extraction