Inductive octet : Set :=
  | OctExact  : bit -> bit -> bit -> bit -> bit -> bit -> bit -> bit -> octet
  | OctRemain : bit -> bit -> bit -> bit -> bit -> bit -> bit -> bit -> octet.
