Nuprl - Pf discrete equality inc 1

(3steps) PrintForm Definitions discrete jlc Sections Support(jlc) Doc

At: discrete equality inc 1

1. T: Type

{T=} (TT)

By: UnfoldTopAb 0 THEN UnivCD

Generated subgoal:

1 2. x: {T=}
x TT

About:

(3steps) PrintForm Definitions discrete jlc Sections Support(jlc) Doc