我正在尝试编写以下函数：
justEq : ∀ {A} -> (x y : A) -> (just x ≡ just y) -> (x ≡ y)
justEq x y pf = {!!}
我不知道怎么写这个。对我来说，它很直观，以至于公理化，但编译器不接受 refl 作为它的证明。
我经常不得不证明这些事情，例如，证明如果两个非空列表相等，那么它们的头是相等的。
对此的一般方法是什么？这是否与康纳·麦克布莱德（Conor McBride）在构造函数的返回中具有函数的"绿色粘性"有关？
解决方案的基础是在pf refl时使用模式匹配，并使用虚线模式y等于x（因为refl的类型！
justEq : ∀ {A} -> (x y : A) -> (just x ≡ just y) -> (x ≡ y)
justEq x .x refl = {!!}
此时，由于模式匹配的y = .x相等性，右侧的孔的类型已统一为(x ≡ x)，这意味着您可以将refl用作类型良好的值，从而给出
justEq x .x refl = refl