Nuprl - Pf discrete equality properties 1

1. T: Type
2. eq: TT
3. x,y:T. eq(x,y) x = y

(x,y:T. eq(x,y) x = y) & eq TT

By: UnhideSqStableHyp1 3

Generated subgoals:

1 SqStable(x,y:T. eq(x,y) x = y)

2 3. x,y:T. eq(x,y) x = y
(x,y:T. eq(x,y) x = y) & eq TT

About:

1	`SqStable(x,y:T. eq(x,y) x = y)`
2	3. `x,y:T. eq(x,y) x = y` `(x,y:T. eq(x,y) x = y) & eq TT`