proposition: Lemma brute_force_works {sz} : forall (P: word sz -> bool), (forallb P (EnumerateWords sz) = true) -> (forall w, P w = true).
proof: Proof. intros * H w. rewrite forallb_forall in H. pose proof (@Enumerate_exhaustive sz). eauto. 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