maybe not a bad idea to mimic this color - they are different lean type (structure, attribute, theorem) <img width="809" height="715" alt="Image" src="https://github.com/user-attachments/assets/c648a272-d379-436d-89bf-d5db91924544" />
maybe not a bad idea to mimic this color - they are different lean type (structure, attribute, theorem)