小编use*_*402的帖子

请注意，这是一个作业，所以最好不要发布完整的解决方案，相反，我只是被卡住了，需要一些关于我接下来应该看什么的提示。

module BST where

open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Relation.Binary
open DecTotalOrder decTotalOrder using () renaming (refl to ?-refl; trans to ?-trans)


data Ord (n m : ?) : Set where
  smaller : n < m -> Ord n m
  equal   : n ? m -> Ord n m
  greater : n > m -> Ord n m

cmp : (n m : ?) -> Ord n m
cmp zero zero       = equal refl
cmp zero (suc …