[ refactor ] proofs in Relation.Nullary.Decidable and a reexport in Function.Related.TypeIsomorphisms

[jamesmckinna]

This a conservative refactoring which:

• cleans up the proof of Relation.Nullary.Decidable.True-↔ to:
  • [ cosmetic ] reuse existing definitions toWitness/fromWitness from Relation.Nullary.Decidable.Core
  • [ add ] appeal to a new local lemma from-to which could be lifted out to top-level?
• [ refactor ] avoids the redundant repetition in Function.Related.TypeIsomorphisms by a public renaming export of the above, cf. [DRY] Refactor algebraic properties of types #2489
• cleans up the proof of Relation.Nullary.Decidable.via-injection to:
  • [ cosmetic] clarify the local opening of the Injection argument injection
• tidies up the relevant imports to reflect the above refactorings

As such, no CHANGELOG required, but could potentially:

• add from-to (suitably named) as top-level lemma
• deprecate Function.Related.TypeIsomorphisms.True↔ in favour of Relation.Nullary.Decidable.True-↔