    Definition binaryExp_ind (b : binaryExp) : P b :=
      binaryExp_rect
        P
        (Forall P)
        (Forall_nil P)
        (Forall_cons (P:=P)) 
        P_BiU32
        P_BiU64
        P_BiF64
        P_BiBytes
        P_BiUTF8
        P_BiArray
        P_BiReserve
        P_BiRecord
        b.
