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

At: decidable iff exists bool function 2 1 1 1
1. T: Type
2. Z: Type
3. P: TZProp
4. g: x:Ty:ZP(x,y)+(P(x,y) False)
5. x: T

y:Z. P(x,y) InjCase(g(x,y) ; true; false)
By: Analyze 0
Generated subgoal:

16. y: Z
P(x,y) InjCase(g(x,y) ; true; false)

About:
bfalsebtrueassertuniondecide
applyfunctionuniversepropimpliesfalseall

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