chore: refactor Elab.StructInst to use mutual
for its structure
s/inductive
s
#6565
copyright-header.yml
on: pull_request
check-lean-files
28s