fix: use reducible transparency when producing no_confusion_type
and injectivity lemmas#812
Open
eric-wieser wants to merge 3 commits intomasterfrom eric-wieser/semireducible-injectivity-lemmas
+34-3
no_confusion_type
and injectivity lemmas#812