T:Type, l1,l2:T List, x:T. l1  l2  (x  l1)  (x  l2)

By:	(RWW (Thm* l1,l2:T List. (Thm* l1  l2  ||l1||||l2|| & (i:. i<||l1||  l1[i] = l2[i]) (0) THEN (Unfold `l_member` 0)

1

1. T : Type 2. l1 : T List 3. l2 : T List 4. x : T 5. ||l1||||l2|| & (i:. i<||l1||  l1[i] = l2[i]) 6. i:. i<||l1|| & x = l1[i]   i:. i<||l2|| & x = l2[i]

2 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html