Modus ponens by strout

module Theorem where open import Function;modus-ponens = id