Require Import a.

Definition b := a.