fact: Fixpoint bytesToBits {n} : (n.-tuple BYTE) -> BITS (n*8) := if n is n'.+1 return n.-tuple BYTE -> BITS (n*8) then fun xs => bytesToBits (behead_tuple xs) ## (thead xs) else fun xs => nilB.
imports: Coq(ZArith.ZArith Strings.String) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp)