Commit 2022-03-26 21:16 7b938899
View on Github →refactor(data/list/basic): Remove many redundant hypotheses (#12950)
Many theorems about last
required arguments proving that certain things were not equal to nil
, when in fact this was always the case. These hypotheses have been removed and replaced with the corresponding proofs.