## Stream: new members

### Topic: How to get lemmas to typecheck

#### Lucas Teixeira (Sep 07 2021 at 14:10):

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 (Sep 07 2021 at 14:12):

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

#### Johan Commelin (Sep 07 2021 at 14:13):

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

#### Johan Commelin (Sep 07 2021 at 14:13):

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

#### Lucas Teixeira (Sep 07 2021 at 14:16):

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 (Sep 07 2021 at 14:27):

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

#### Lucas Teixeira (Sep 07 2021 at 14:30):

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

Last updated: Dec 20 2023 at 11:08 UTC