module exampletrue where
  
data ⊤ : Set where
  true : ⊤ 

record ⊤' : Set where


true' : ⊤'
true' = record { }