1. A : Type
2. a : A
3. a' : A
4. x : a = a'
  x = *

By:	Refine RULE  H, x:(p = q  A), J   C ext t RULE  H,BY equalityElimination #$i RULE  H,H, x:(p = q  A), J[*/x]  C[*/x] ext t RuleArgs:[4:n]

1

* = *  (a = a')

2 steps

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