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

At: is intersection wf 1 2
1. T: Type
2. eq: {T}
3. L: T List
4. u: T
5. v: T List
6. M:T List. v(eq)M Type

M:T List. (u.v)(eq)M Type
By:
Analyze 0
THEN
AbReduce 0
Generated subgoal:

17. M: T List
(u(eq) M xv.x(eq) M) Type

About:
listconsassertuniversememberorall

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