1. T : Type
2. x : T
3. T List
4. y:T. x = y  x = y
5. u : T
6. v : T List
7. (x  v)  (x  v)
  (x  [u / v])  (x  [u / v])

By:	AllHyps (InstHyp [u]) THEN Analyze -1 THEN RWW Thm* l:T List, a,x:T. (x  [a / l])  x = a  (x  l) 0 THEN SimpConcl

None

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