Closed GeoffreySangston closed 1 week ago
Looks like the ~T1 trait is also redundant, but it's a non-trivial sequence of reductions so I'll leave it, unless someone says it's better to remove it.
Edit: I decided to remove the ~T1 trait since the argument was really the same observation as 'Has a generic point' but with a weaker conclusion.
Seems straightforward. Just have to look for redundant traits now.