等式证明中的模式匹配(析构函数)

Question

data T = A String | B String
p : ((A s) = (A s')) -> (s = s')

如果我有(A s) = (A s')，如何获得s = s'？

附言：我是伊德里斯的新手。请随意编辑我的问题的代码风格或添加相关的关键字。

Answer 1

Refl:上的模式匹配

data T = A String | B String
p : ((A s) = (A s')) -> (s = s')
p Refl = Refl