fix: use reducible transparency when producing `no_confusion_type` and injectivity lemmas

[eric-wieser]

The relevant test case is

def wrapped_nat (n : nat) := nat

structure with_wrapped : Type :=
(n : nat)
(m : wrapped_nat n)

#check with_wrapped.mk.inj_eq

The diff due to this PR is

 ∀ {n : ℕ} {m : wrapped_nat n} {n' : ℕ} {m' : wrapped_nat n'},
-   with_wrapped.mk n m = with_wrapped.mk n' m' = (n = n' ∧ m = m'))
+   with_wrapped.mk n m = with_wrapped.mk n' m' = (n = n' ∧ m == m'))

which is an improvement since m and m' are not intended to be equal types.

It's not immediately clear to me whether this will stop the particular defeq check that is causing trouble in this motivating Zulip thread.