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

At: decidable iff exists bool function 1
1. T: Type
2. P: TProp
3. x:T. Dec(P(x))

f_p:(T). x:T. P(x) f_p(x)
By:
Repeat (Unfolds [`decidable`;`or`;`not`;`all`;`implies`] 3)
THEN
RenameVar `g' 3
Generated subgoal:

13. g: x:TP(x)+(P(x)False)
f_p:(T). x:T. P(x) f_p(x)

About:
boolassertdecidableapplyfunctionuniversepropallexists

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