proposition: Lemma EncodeBoundedNat8_simplify : forall (w: BoundedNat 8) c, EncodeBoundedNat w c = ({| padding := 0; front := WO; paddingOK := Lt.lt_0_Sn 7; byteString := (BoundedNat8ToByte w :: nil) |}, addE c 8).
proof: Proof. unfold EncodeBoundedNat, encode_word_Impl; intros. rewrite encode_char', NToWord_of_nat. reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.BinEncoders.Basics Coq.Lists.List Bedrock.Word Program Nomega