    Fixpoint binaryExp_rect (b : binaryExp) : P b :=
      let
        fix expForAll (xs : list binaryExp) : P_list xs :=
          match xs as rxs return (P_list rxs) with
          | []        => @P_nil
          | (y :: ys) => @P_cons y ys (binaryExp_rect y) (expForAll ys)
          end
      in let
        fix forAllSnd (fs : list (string * binaryExp)) : P_list (map snd fs) :=
          match fs as rf return P_list (map snd rf) with
          | []             => @P_nil
          | ((_, y) :: ys) => @P_cons y (map snd ys) (binaryExp_rect y) (forAllSnd ys)
          end
      in
        match b with
        | BiU32 c     => P_BiU32 c
        | BiU64 c     => P_BiU64 c
        | BiF64 c     => P_BiF64 c
        | BiBytes bs  => P_BiBytes bs
        | BiUTF8 bs   => P_BiUTF8 bs
        | BiArray es  => P_BiArray es (expForAll es)
        | BiReserve c => P_BiReserve c
        | BiRecord fs => P_BiRecord fs (forAllSnd fs)
        end.
