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

At: not not rw 1
1. T: Type
2. P: TProp
3. x:T. Dec(P(x))
4. x: T

P(x) P(x)
By: Witness3 x
Generated subgoal:

13. x: T
4. Dec(P(x))
P(x) P(x)

About:
decidablefunctionuniversepropall

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