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

At: is intersection implies exists element


T:Type, eq:{T=}, L,M:T List. L(eq)M (x:{x:T| x(eq) L }. x(eq) M)

By: UnivCD

Generated subgoal:

11. T: Type
2. eq: {T=}
3. L: T List
4. M: T List
5. L(eq)M
x:{x:T| x(eq) L }. x(eq) M

About:
listassertsetuniverseimpliesallexists

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