A:Type, x,y:A, P:(AProp), i,j:.
  P(if i=j x else y fi)  P(if i=j x else y fi)

1

1. A : Type 2. x : A 3. y : A 4. P : AProp 5. i :  6. j :  7. P(if i=j x else y fi)   P(if i=j x else y fi)

3 steps

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