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

At: decidable iff exists bool function 1 1 1 1 1
1. T: Type
2. P: TProp
3. g: x:TP(x)+(P(x)False)
4. x: T
5. y1: P(x)False
6. inr(y1) = g(x)
7. P(x)

False
By: Analyze 5
Generated subgoals:

None

About:
unioninrapplyfunctionuniverseequalpropfalse

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