proposition: Lemma encode_byte_simplify : forall (w: word 8) c, encode_word_Impl w c = ({| padding := 0; front := WO; paddingOK := Lt.lt_0_Sn 7; byteString := w :: nil |}, addE c 8).
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