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

At: decidable iff exists bool function 2 1 1 1 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
6. y: Z
7. y1: y:ZP(x,y)+(P(x,y) False)
8. y1 = g(x)
9. y2: P(x,y)+(P(x,y) False)
10. y2 = y1(y)

P(x,y) InjCase(g(x,y) ; true; false)
By:
HypSubst 8 10
THEN
RevHypSubst 10 0
Generated subgoal:

110. y2 = g(x,y)
P(x,y) InjCase(y2 ; true; false)

About:
bfalsebtrueassertuniondecide
applyfunctionuniverseequalpropimpliesfalse

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