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

At: discrete implies discrete equality 1 1 1 1 2
1. T: Type
2. g: x,y:T. (x = y)+(x = y)

x,y:T. (x,y. InjCase(g(x,y) ; true; false))(x,y) x = y
By: UnivCD
Generated subgoal:

13. x: T
4. y: T
(x,y. InjCase(g(x,y) ; true; false))(x,y) x = y

About:
bfalsebtrueassertuniondecide
lambdaapplyuniverseequalall

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