fix: respect type reducibility when generating injectivity lemmas

[eric-wieser]

The relevant test case is:

def WrappedNat (_n : Nat) := Nat

structure WithWrapped : Type :=
(n : Nat)
(m : WrappedNat n)

#check WithWrapped.mk.injEq
#print WithWrapped.noConfusionType

The diff due to this PR is intended to be

 WithWrapped.mk.injEq (n : Nat) (m : WrappedNat n) (n : Nat) (m : WrappedNat n) :
-  ({ n := n, m := m } = { n := n, m := m }) = (n = n ∧ m = m)
+  ({ n := n, m := m } = { n := n, m := m }) = (n = n ∧ HEq m m)
@[reducible] protected def WithWrapped.noConfusionType.{u} : Sort u → WithWrapped → WithWrapped → Sort u :=
-fun P v1 v2 => WithWrapped.casesOn v1 fun n m => WithWrapped.casesOn v2 fun n_1 m_1 => (n = n_1 → m = m_1 → P) → P
+fun P v1 v2 => WithWrapped.casesOn v1 fun n m => WithWrapped.casesOn v2 fun n_1 m_1 => (n = n_1 → HEq m m_1 → P) → P

This forward-ports https://github.com/leanprover-community/lean/pull/812.

For now, I am just creating this to see if it passes CI, since CI appears not to run on my branch in a fork.