Pattern-match (destructure) in equality proof

Question

data T = A String | B String

p : ((A s) = (A s')) -> (s = s')

If I have (A s) = (A s'), how do I obtain s = s'?

P.S. I'm new to Idris. Feel free to edit my question for code style or to add pertinent keywords.

user_6369276 · Answer

Pattern match on Refl:

data T = A String | B String

p : ((A s) = (A s')) -> (s = s')
p Refl = Refl