(23steps) PrintForm Definitions Lemmas list 3 jlc Sections Support(jlc) Doc

At: not list all not iff list exists 1
1. T: Type
2. P: TProp
3. x:T. Dec(P(x))
4. L: T List

xL.(P(x)) xL.P(x)
By:
Analyze 0
THEN
Analyze 0
Generated subgoals:

15. xL.(P(x))
xL.P(x)
25. xL.P(x)
xL.(P(x))

About:
listdecidablefunctionuniversepropall

(23steps) PrintForm Definitions Lemmas list 3 jlc Sections Support(jlc) Doc