A (partial) Agda port of the RGref Coq DSL