Not-irrelevant proofs?

[goens]

In EffectKind.lean we have a bunch of lemmata that take proofs of known theorems as statements, e.g.

@[simp] theorem liftEffect_pure_impure [Monad m] (hle : pure ≤ impure) :
    liftEffect hle (α := α) (m := m) = Pure.pure 

Can we get rid of these argument like hle which is a theorem (pure_le impure)? @bollu suggests making them default arguments, we can also look into that option.

[bollu]

@hargoniX gave me an explanation of how something similar bit him:

It's because of the type of the proof, the type of the proof itself contains an occurence of the term that we generalize over, let's call this term t when we generalize t into t' the generalize tactic does of course not see that it has to fix this proof term so we end up with a proof about t where now a proof about t' is expected. In an extensional type theory this would of course be no problem but we are not extensional^^

If we s/generalize/rewrite, this explains the folklore that @alexkeizer was told.