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

At: decidable sublist 1
1. T: Type
2. eq: {T}
3. eq TT
4. L: T List
5. M: T List

Dec(L(eq)M)
By:
MoveToConcl -1
THEN
ListInd -1
THEN
Reduce 0
Generated subgoals:

None

About:
listbooldecidablefunctionuniversemember

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