Idempotency of entailment
is a property of logical systems
that states that one may derive the same consequences from many instances of a hypothesis as from just one. In sequent calculi this property can be captured by a structural rule
and in such systems one may say that entailment is idempotent just in case contraction is an admissible rule
Rule of Contraction: from
A,C,C -> B
A,C -> B.
Or in sequent calculus notation,