Nuprl - Proof: strict part irrefl

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: strict part irrefl

T:Type, R:(T

Prop), a,b:T. strict_part(x,y.R(x,y);a;b)

a = b

By:	Unfolds [`not`;`strict_part`] 0 THEN RepD

Generated subgoal:

1 1. T : Type
2. R : TTProp
3. a : T
4. b : T
5. R(a,b)
6. R(b,a)
7. a = b
False
1 step

About:

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