Lemma forall_map_binarySize : forall es,
  Forall (fun b : binaryExp => binarySize b mod 4 = 0) es
    <-> Forall (fun n => n mod 4 = 0) (map binarySize es).
Proof.
  (* Proof omitted for brevity; see Binary.v for proofs. *)
Qed.
