 Logical implication

Logical implication forms the proposition $A\to B$. In intuitionistic logic its proof consists of a construction that transforms any proof of $A$ into a proof of $B$.