How to get lemmas to typecheck

Stream: new members

[Lucas Teixeira]

So I've prepared a lemma

lemma honey : (¬q → ¬p) → (p → q) :=
  (assume mh: (¬q → ¬p),
   show (p → q),
   from or.cases_on (em q)
     (λ hq: q, λ hp: p, hq)
     (λ hnq: ¬q, λ hp: p, absurd hp (mh hnq))
  )

to support the following theorem

theorem mint : (((p → q) → p) → p) :=
  (assume mh: (p → q) → p,
   or.cases_on (em p)
     (λ hp: p, hp)
     (λ hnp: ¬p, absurd (mh (honey (λ hnq: ¬q, hnp)) hnp))
  )

but I get the error

type mismatch at application
  honey _
term
  λ (hnq : ¬q), hnp
has type
  ¬q → ¬p : Prop
but is expected to have type
  Prop : Type

What gives??

[Johan Commelin]

@Lucas Teixeira Probably p and q are explicit arguments of honey.

[Johan Commelin]

Do you have variables (p q : Prop) somewhere above that lemma?

[Johan Commelin]

If you turn it into variables {p q : Prop} the error should go away.

[Lucas Teixeira]

Johan Commelin Yes that worked! (Although now I see I have further problems with my proof haha). Could you give some indication as to why that worked?

[Johan Commelin]

This should be somewhere in #tpil, looks like S6.5 is useful

[Lucas Teixeira]

Ahh, gotcha. Still a couple of chapters behind. Thank you for the help!