Nuprl - Pf list iso commutative 1

1. T: Type
2. eq: {T}
3. L: T List
4. M: T List

L(~eq)M M(~eq)L

By: Equivalence 2 THEN Analyze 0 THEN Analyze 0 THEN UnfoldTopAb 0 THEN UnfoldTopAb -1

Generated subgoals:

None

About: