feat(library/init/core): allow lists of proofs

[eric-wieser]

With upstream changes to mathlib, this would allow fintype some_prop, which would in turn allow proofs to be used to index finite things like matrices or summations.

[gebner]

IIRC it was intentional that the type parameter of list and option is in Type instead of Sort, as this simplifies type inference. Have you tried compiling mathlib with this change?

[eric-wieser]

I have not at any point tried to build lean itself locally, and was relying on CI to do that. Presumably once this build passes, I can create a mathlib branch that points to this branch, and have CI test that too?

[gebner]

You need to make a tag for the CI to upload a release. Please make the tag on your own fork.

[eric-wieser]

Build is full of failures with trivial goals that simp isn't closing:

/home/runner/work/lean/lean/library/init/data/list/lemmas.lean:25:3: error: tactic failed, there are unsolved goals
state:
case list.cons
α : Type u,
t_hd : α,
t_tl : list α,
t_ih : t_tl ++ nil = t_tl
⊢ t_hd = t_hd ∧ t_tl = t_tl

I guess I'll have to try this locally...