 Implication elimination rule

From $A\to B$ and $A$, implication elimination derives $B$. Under the Curry-Howard correspondence, this is application: from lambda terms $f:A\to B$ and $a:A$ form $fa:B$.