feat: split [implicit_reducible] into [instance_reducible] and [implicit_reducible] tiers#13637

kim-em wants to merge 4 commits into

leanprover:masterleanprover/lean4:masterfrom

kim-em:split_implicit_reduciblekim-em/lean4:split_implicit_reducibleCopy head branch name to clipboard