Summary
- merged
- more abstract naming
- tuned
- workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar
- a derived rule combining unoverload and internalize_sort
- merged
- fixed a name clash
- merged
- the last of the infinite product proofs
- merged
- proved avl for map (finally); tuned