The Coq back end translates quick check properties to theorems. Generate functions producing a corresponding equality type (`_≡_`) in the Agda back end.