proposition: Lemma brute_force_works' {sz} : forall (P: word sz -> Prop) (P': word sz -> bool), (forall w, P' w = true -> P w) -> (forallb P' (EnumerateWords sz) = true) -> (forall w, P w).
proof: Proof. intros * correctB forallB w. apply correctB; revert w. apply brute_force_works; assumption. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat List Bedrock.Word Coq.ZArith.ZArith Coq.micromega.Psatz NArith NArithRing ZArith ZArithRing Program Coq.micromega.Psatz AlignedByteString Permutation