experiment: forbid large elim of recursive Prop inductives#13851

nomeata wants to merge 1 commit into

masterleanprover/lean4:masterfrom

joachim/no-large-elimleanprover/lean4:joachim/no-large-elimCopy head branch name to clipboard