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

At: list all tail 1 1
1. T: Type
2. P: TProp
3. L: T List
4. x: T
5. P(x) & xL.P(x)

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

None

About:
listfunctionuniversepropand

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