Inductive octet : Set :=
  | OctExact  : bit → bit → bit → bit → bit → bit → bit → bit → octet
  | OctRemain : bit → bit → bit → bit → bit → bit → bit → bit → octet.
