(* This file has no dependencies. *)

Definition a := 0.