fact: Fixpoint seqBytesToBits (xs : seq BYTE) : BITS (size xs*8) := if xs is x::xs' return BITS (size xs*8) then seqBytesToBits xs' ## x else nilB.
imports: Coq(ZArith.ZArith Strings.String) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp)