Nuprl - Pf decidable sublist

T:Type, eq:{T}, L,M:T List. Dec(L(eq)M)

By: Analyze 0 THEN Analyze 0 THEN EquivT -1 THEN UnivCD

Generated subgoal:

1 1. T: Type
2. eq: {T}
3. eq TT
4. L: T List
5. M: T List
Dec(L(eq)M)

About: