(* this file depends on b.v and c.v *)

Require Import b c.

Definition a := 4.