(15steps) PrintForm Definitions list 3 jlc Sections Support(jlc) Doc

At: decidable list exists 1 2 1 1 1 2 2
1. T: Type
2. P: TProp
3. L: T List
4. u: T
5. v: T List
6. xv.P(x)
7. P(u)

P(u) xv.P(x) (P(u) xv.P(x))
By:
Unfold `not` 0
THEN
DNth 2 0
Generated subgoal:

18. P(u) xv.P(x)
False

About:
listfunctionuniverseproporfalse

(15steps) PrintForm Definitions list 3 jlc Sections Support(jlc) Doc