(* The following defines the absolute name b.a *)

Definition a := 1.