Modus ponens by ikegami__

-- ASCII modus ponens
-- Recommend highly to use Unicode characters in Agda;
-- especially for the Agda standard library

module Theorem where

import Level

modus-ponens : forall {a b} -> {P : Set a} {Q : Set b} -> (P -> Q) -> P -> Q
modus-ponens f = f