Logical implication (source code)

= Logical implication
{title2=$\to$}

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$.