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