Some more small progress on diamonds for 'arrowless' inductive types. I still think inference might be feasible, but it's tricky.