(* This file depends on nothing. *)

Definition a := 0.