[Agda] Type-preserving renaming and substitutions for a dependently typed lambda calculus.

[effectfully]

Hello. I was studying different deep embeddings of a dependently typed
lambda calculus, and I found three works: Nils Anders Danielsson's
thesis, James Chapman's thesis and Typed Syntactic Meta-programming by
Dominique Devriese and Frank Piessens (I'm not counting Conor
McBride's Outrageous but Meaningful Coincidences). However the first
work uses explicit weakening for the base encoding (there is also a
conversion to implicit terms), the second work moreover uses explicit
substitutions, and the third work is based on a homogeneous datatype,
which represents both types and terms.
I wrote some code in order to understand what are the problems with
the natural representation (a bunch of mutually defined datatypes with
the usual semantics) equipped with implicit weakening and
substitutions. A module that contains implicit weakening can be found
at [1] (some explanations can be found at [2]), but there is no
substitutions stuff and no applications at all. The code looks simple
and natural until the proving part begins, which is somewhat
complicated. I also wrote a sketch for the full system (the same +
applications and hence substitutions) with all proofs being postulated
[3].
So I'm wondering, if there is something silly with my representation,
that cause this amount of proving, and if there exist works, which
elarobate this kind of encoding.
Thank you for your attention.

[1] https://github.com/effectfully/Ouroboros/blob/master/Weakening/Main.agda
[2] https://github.com/effectfully/Ouroboros/blob/master/readme.md
[3] https://github.com/effectfully/Ouroboros/blob/master/Full/Sketch.agda