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

At: is member cons

T:Type, eq:{T}, t:T, L:T List. t(eq) (t.L)
By:
AbReduce 0
THEN
UnivCD
Generated subgoal:

11. T: Type
2. eq: {T}
3. t: T
4. L: T List
if eq(t,t) true else t(eq) L fi

About:
listconsbtrueifthenelseassertapplyuniverseall

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