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

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

xL.P(x)
By: Rewrite (HigherC list_all_unrollC) 5
Generated subgoal:

15. P(x) & xL.P(x)
xL.P(x)

About:
listconsfunctionuniverseprop

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