proposition: Lemma encode_word8_Impl_length : forall (w: word 8) c, List.length (byteString (fst (encode_word_Impl w c))) = 1.
proof: Proof. unfold encode_word_Impl; intros; rewrite encode_char'; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.BinEncoders.Basics Coq.Lists.List Bedrock.Word Program Nomega