What is higher order natural deduction? Well, what you do when you use higher order constructive type theory as a logical framework is essentially bring to the foreground the consequence relation which connects hypothesis to a conclusion in an object logical system.
And what we do is we model this by the arrow type constructor of the meta-language. And so we somehow import some structural rules, such as weakening contraction, substitutivity. These are inherited or delegated, you may say, to meta-language.