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

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

P(x) InjCase(g(x) ; true; false)
By: Witness3 x
Generated subgoal:

15. y: P(x)+(P(x)False)
6. y = g(x)
P(x) InjCase(g(x) ; true; false)

About:
bfalsebtrueassertunion
decideapply
functionuniversepropfalse

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