let and_intro : ∀ (p q : Prop),
                  p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q :=
      λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c),
        H H1 H2,
    and_elim_left : ∀ (p q : Prop),
                      (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → p :=
      λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q),
        H p (λ (H1 : p) (H2 : q), H1),
    and_elim_right : ∀ (p q : Prop),
                       (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → q :=
      λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q),
        H q (λ (H1 : p) (H2 : q), H2)
in and_intro :
  ∀ (p q : Prop),
    p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q
let1.lean:16:10: error: type mismatch at application
  let and_intro : ∀ (p q : Prop),
                    p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) q p :=
        λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c),
          H H1 H2,
      and_elim_left : ∀ (p q : Prop),
                        (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → p :=
        λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q),
          H p (λ (H1 : p) (H2 : q), H1),
      and_elim_right : ∀ (p q : Prop),
                         (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → q :=
        λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q),
          H q (λ (H1 : p) (H2 : q), H2)
  in and_intro
term
  λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c),
    H H1 H2
has type
  ∀ (p q : Prop),
    p → q → (∀ (c : Prop), (p → q → c) → c)
but is expected to have type
  ∀ (p q : Prop),
    p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) q p