Cut

Tested with Agda 2.6.2, Agda standard library 1.7.

• The cut theorem is here.
• The proof follows this lecture note by Frank Pfenning, except each sequent calculus derivation is indexed by its size to pass Agda's termination check.
• By the cut theorem, we can prove each natural deduction derivation is also a sequent calculus derivation, since sequent calculus is consistent, so natural deduction is also consistent.