Nuprl - Pf decidable list iso

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

By: Analyze 0 THEN Analyze 0 THEN EquivT -1 THEN UnivCD THEN Unfold `list_iso` 0

Generated subgoal:

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

About: