寻找包含列表可判定相等性的 Agda 模块

问题描述

给定两个列表 xs 和 ys，我想获得 Dec(xs ≡ ys) 的值。 有谁知道包含这种操作符的标准库模块的名称吗？

解决方法

它在 Data.List.Properties 中，名为 ≡-dec