variables P Q R B : Prop

example: P → (P → Q) → Q := λx g, g x

theorem foo : P → (P → Q) → Q := λx g, g x

example: (P→R)∨(Q→R) → (P∧Q → R) :=
  λ(x: (P→R)∨(Q→R)),                    -- outer → intro
    λ(y: P∧Q),                            -- inner → intro
      match x with                         -- ∨ elim begins
      | or.inl f := f (and.elim_left y)
      | or.inr g := g (and.elim_right y)
      end                                  -- ∨ elim ends, conclude R

example: ¬(P∨Q) → ¬P :=
  λ(x: ¬(P∨Q)),         -- outer → intro
    λ(p: P),             -- ¬P intro = P→false intro
      x (or.inl p)       -- x: P∨Q→false

axiom pierce {s t : Prop} : ((s -> t) -> s) -> s

example: B∨¬B :=
  pierce (λ(x: B∨¬B → false),
           (or.inr (λ(b: B), x (or.inl b)) : B∨¬B))