(6steps) PrintForm Definitions core 3 jlc Sections Support(jlc) Doc

At: decidable iff exists bool function 1 1
1. T: Type
2. P: TProp
3. g: x:TP(x)+(P(x)False)

f_p:(T). x:T. P(x) f_p(x)
By:
Witness x.InjCase(g(x) ; true; false)
THEN
Analyze 0
THEN
Reduce 0
Generated subgoal:

14. x: T
P(x) InjCase(g(x) ; true; false)

About:
boolbfalsebtrueassertuniondecidelambda
applyfunctionuniversepropfalseallexists

(6steps) PrintForm Definitions core 3 jlc Sections Support(jlc) Doc