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

At: discrete implies bool equality 1 1
1. T: Type
2. g: Discrete{T}

f:(TT). x,y:T. f(x,y) x = y
By: Repeat (Unfolds [`discrete`;`decidable`;`or`] 2)
Generated subgoal:

12. g: x,y:T. (x = y)+(x = y)
f:(TT). x,y:T. f(x,y) x = y

About:
boolassertapplyfunctionuniverseequalallexists

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