2014-07-22 09:43:18 -07:00
|
|
|
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),
|
2014-07-09 18:47:10 -07:00
|
|
|
H H1 H2,
|
2014-07-22 09:43:18 -07:00
|
|
|
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),
|
2014-07-09 18:47:10 -07:00
|
|
|
H p (λ (H1 : p) (H2 : q), H1),
|
2014-07-22 09:43:18 -07:00
|
|
|
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),
|
2014-07-09 18:47:10 -07:00
|
|
|
H q (λ (H1 : p) (H2 : q), H2)
|
|
|
|
in and_intro :
|
2014-07-22 09:43:18 -07:00
|
|
|
∀ (p q : Prop),
|
|
|
|
p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q
|
2014-07-25 09:44:40 -07:00
|
|
|
let1.lean:16:10: error: type mismatch at application
|
2014-07-26 21:00:22 -07:00
|
|
|
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
|
2014-07-28 07:08:12 -07:00
|
|
|
term
|
|
|
|
λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c),
|
|
|
|
H H1 H2
|
|
|
|
is expected of type
|
2014-07-22 09:43:18 -07:00
|
|
|
∀ (p q : Prop),
|
|
|
|
p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) q p
|
2014-07-28 07:08:12 -07:00
|
|
|
but is given type
|
2014-07-22 09:43:18 -07:00
|
|
|
∀ (p q : Prop),
|
|
|
|
p → q → (∀ (c : Prop), (p → q → c) → c)
|