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

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

f:{T=}. True
By: Witness x,y. InjCase(g(x,y) ; true; false) THENL [Id;Auto;Auto]
Generated subgoal:

1 (x,y. InjCase(g(x,y) ; true; false)) {T=}

About:
bfalsebtrueuniondecidelambda
applyuniverseequalmembertrueallexists

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