Modus ponens by trigott

module Theorem where

  import Level

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