To cope with the lambda calculus's syntactic restrictions, m shall denote the implication function taking two parameters, that is, the lambda term ((m A) B) shall be equivalent to the usual infix notation A \to B.
