Completeness of atomic initial sequents
In sequent calculus, the completeness of atomic initial sequents states that initial sequents can be derived from only atomic initial sequents . This theorem plays a role analogous to eta expansion in lambda calculus, and dual to cut elimination and beta reduction. Typically it can be established by induction on the structure of, much more easily than cut elimination.