module Record where module M where record A : Set where constructor a open M record B : Set where record C : Set where constructor c x : A x = a y : C y = record {}