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

At: is intersection wf 1 2 1
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
7. M: T List

(u(eq) M xv.x(eq) M) Type
By:
Auto
THEN
HypBackchain
THEN
Trivial
Generated subgoals:

None

About:
listassertuniversememberorall

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