proposition: Lemma Enumerate_exhaustive {sz} : forall w: word sz, In w (EnumerateWords sz).
proof: Proof. induction w. - simpl; tauto. - simpl; rewrite in_app_iff. destruct b; [left|right]; rewrite in_map_iff; exists w; tauto. 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