Modus ponens by Rotsor

module Theorem where import Level;modus-ponens = λ{a}{P : Set a}(x : P)→ x