Nuprl - Pf discrete implies discrete equality 1

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

At: discrete implies discrete equality 1

1. T: Type

Discrete{T} (f:{T=}. True)

By: Analyze 0

Generated subgoal:

1 2. Discrete{T}
f:{T=}. True

About:

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