Agda template
data
Example
:
Set
where
Ok
:
Example