Nuprl - Pf discrete implies discrete equality 1 1

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

At: discrete implies discrete equality 1 1

1. T: Type
2. Discrete{T}

f:{T=}. True

By: RenameVar `g' 2 THEN Repeat (Unfolds [`discrete`;`decidable`;`or`] 2)

Generated subgoal:

1 2. g: x,y:T. (x = y)+(x = y)
f:{T=}. True

About:

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