completeness of atomic initial sequents

In sequent calculus, the completeness of atomic initial sequents states that initial sequents {{math|A ⊢ A}} (where {{math|A}} is an arbitrary formula) can be derived from only atomic initial sequents {{math|p ⊢ p}} (where {{math|p}} is an atomic formula). 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 {{math|A}}, much more easily than cut elimination.