1. A:Type, eq:EqDecider(A), B:(AType), P:(x:AB(x)Prop), x:A, v:B(x).
1. ydom(x : v). w=x : v(y)   P(y,w)  P(x,v)
  A:Type{i}, eq:EqDecider(A), P:(AType{i}Prop{i}), x:A, v:Type{i}.
  ydom(x : v). w=x : v(y)   P(y,w)  P(x,v)

By:	RepeatFor 2 (ParallelOp -1) THEN InstHyp [x. Type{i}] -1

None

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