Modus ponens by Lost_dog_

module Theorem where

import Level

modus-ponens : ∀ {a b} {P : Set a} {Q : Set b} → (P → Q) → P → Q
modus-ponens = λ z → z