1. T : Type
2. a : T
3. a' : T
4. b : T List
5. b' : T List
6. [a / b] = [a' / b']
  a = a'

By:	ApFunToHypEquands `lst' if 0<||lst|| hd(lst) else a fi T -1 THENA Try SplitOnConclITE THEN Reduce -1 THEN RepeatFor 2 (MoveToConcl -1 THEN SplitOnConclITE)

None

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