Yet Another Bijection Between Sequent Calculus and Natural Deduction

This work shows a bijection between sequent calculus and natural deduction for intuitionistic propositional logic so far as normal and cut-free derivations are concerned.