Experiment on exporting Agda into Haskell(a la Coq) based on Agda 2.3.2.2