proposition: Lemma encode_char' : forall w, encode_word' 8 w = {| front := WO; paddingOK := Lt.lt_0_Sn _; byteString := w :: nil |}.
proof: Proof. intros; change 8 with (8+0); rewrite encode_char. shatter_word w; simpl; rewrite ByteString_transform_id_right. reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.BinEncoders.Basics Coq.Lists.List Bedrock.Word Program Nomega