is mentioned by

Thm* (x,y:T. Dec(x = y)) (s:T List, z:T. (z s) (s1,s2:T List. s = (s1 @ [z / s2]) & (z s1)))	[l_member_decomp2]
Thm* x,y:A+B. (a1,a2:A. Dec(a1 = a2)) (b1,b2:B. Dec(b1 = b2)) Dec(x = y)	[decidable__equal_union]

In prior sections: core int 1 bool 1 int 2 rel 1 mb basic mb nat mb list 1 num thy 1 mb list 2

Try larger context: Graphs