fact: Fixpoint ByteString_into_queue' {sz} (chars : ByteBuffer.t sz) {struct chars} : BitString := match chars return BitString with | Vector.nil => [ ] | Vector.cons char' _ chars' => app (wordToQueue char') (ByteString_into_queue' chars') end.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.NArith.NArith Coq.Arith.Arith Coq.Numbers.Natural.Peano.NPeano Coq.Logic.Eqdep_dec Fiat.Narcissus.Common.Specs Fiat.Narcissus.BinLib.Core Fiat.Narcissus.Formats.ByteBuffer