Nuprl - Proof: discrete vs bool 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: discrete vs bool 1

1. A : Type

(A Discrete)

(

e:(A

x,y:A. (x e y)

x = y)

By:	Use:[A \| x,y. x = y A] Inst: Thm* E:(TTProp). Thm* (x,y:T. Dec(E(x,y))) (f:(TT). x,y:T. (x f y) E(x,y)) THEN ReduceSOAps Hyp:-1

Generated subgoal:

1 2. (x,y:A. Dec(x = y)) (f:(AA). x,y:A. (x f y) x = y)
(A Discrete) (e:(AA). x,y:A. (x e y) x = y)
1 step

About:

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