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

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

InjCase(g(x,y) ; true; false)
By:
Reduce 0
THEN
UnivCD
Generated subgoal:

1 InjCase(g(x,y) ; true; false)

About:
boolbfalsebtrueuniondecide
applyuniverseequalmemberall

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