Require A.

Definition c := A.b.
Lemma foo : c = false.
Proof.
reflexivity.
Qed.