Identity weakening rule
= Identity weakening rule
{title2=$\dfrac{C\quad D}{C}$}
The rule with premises $C,D$ and conclusion $C$ retains the first derivation while allowing an unused second assumption. Under the <Curry-Howard correspondence>, the output term is the first premise term, with the enlarged context. This allows a <lambda abstraction> whose bound variable does not occur in its body.