En el cálculo de secuencias , la completitud de las secuencias iniciales atómicas establece que las secuencias iniciales A ⊢ A (donde A es una fórmula arbitraria ) pueden derivarse únicamente de las secuencias iniciales atómicas p ⊢ p (donde p es una fórmula atómica ). Este teorema desempeña un papel análogo a la expansión eta en el cálculo lambda , y dual a la eliminación por corte y la reducción beta . Normalmente, se puede establecer por inducción sobre la estructura de A , mucho más fácilmente que la eliminación por corte.