2013-12-16 06:00:26 +00:00
|
|
|
Set: pp::colors
|
|
|
|
|
Set: pp::unicode
|
|
|
|
|
Assumed: A
|
|
|
|
|
Assumed: B
|
|
|
|
|
Assumed: C
|
|
|
|
|
Assumed: P
|
|
|
|
|
Assumed: F1
|
|
|
|
|
Assumed: F2
|
|
|
|
|
Assumed: H
|
|
|
|
|
Assumed: a
|
2013-12-19 20:46:14 +00:00
|
|
|
Eta (F2 a) : (λ x : B, F2 a x) == F2 a
|
2013-12-16 06:00:26 +00:00
|
|
|
Abst (λ a : A, Trans (Symm (Eta (F1 a))) (Trans (Abst (λ b : B, H a b)) (Eta (F2 a)))) :
|
|
|
|
|
(λ x : A, F1 x) == (λ x : A, F2 x)
|
|
|
|
|
Abst (λ a : A, Abst (λ b : B, H a b)) : (λ (x : A) (x::1 : B), F1 x x::1) == (λ (x : A) (x::1 : B), F2 x x::1)
|
|
|
|
|
Proved: T1
|
|
|
|
|
Proved: T2
|
|
|
|
|
Proved: T3
|
|
|
|
|
Proved: T4
|
|
|
|
|
Theorem T1 : F1 = F2 := Abst (λ a : A, Abst (λ b : B, H a b))
|
|
|
|
|
Theorem T2 : (λ (x1 : A) (x2 : B), F1 x1 x2) = F2 := Abst (λ a : A, Abst (λ b : B, H a b))
|
|
|
|
|
Theorem T3 : F1 = (λ (x1 : A) (x2 : B), F2 x1 x2) := Abst (λ a : A, Abst (λ b : B, H a b))
|
|
|
|
|
Theorem T4 : (λ (x1 : A) (x2 : B), F1 x1 x2) = (λ (x1 : A) (x2 : B), F2 x1 x2) :=
|
|
|
|
|
Abst (λ a : A, Abst (λ b : B, H a b))
|
|
|
|
|
Set: lean::pp::implicit
|
2013-12-22 01:02:16 +00:00
|
|
|
Theorem T1 : @eq (A → B → C) F1 F2 :=
|
|
|
|
|
@Abst A (λ x : A, B → C) F1 F2 (λ a : A, @Abst B (λ x : B, C) (F1 a) (F2 a) (λ b : B, H a b))
|
|
|
|
|
Theorem T2 : @eq (A → B → C) (λ (x1 : A) (x2 : B), F1 x1 x2) F2 :=
|
|
|
|
|
@Abst A
|
|
|
|
|
(λ x : A, B → C)
|
|
|
|
|
(λ (x1 : A) (x2 : B), F1 x1 x2)
|
|
|
|
|
F2
|
|
|
|
|
(λ a : A, @Abst B (λ x : B, C) (λ x2 : B, F1 a x2) (F2 a) (λ b : B, H a b))
|
|
|
|
|
Theorem T3 : @eq (A → B → C) F1 (λ (x1 : A) (x2 : B), F2 x1 x2) :=
|
|
|
|
|
@Abst A
|
|
|
|
|
(λ x : A, B → C)
|
|
|
|
|
F1
|
|
|
|
|
(λ (x1 : A) (x2 : B), F2 x1 x2)
|
|
|
|
|
(λ a : A, @Abst B (λ x : B, C) (F1 a) (λ x2 : B, F2 a x2) (λ b : B, H a b))
|
|
|
|
|
Theorem T4 : @eq (A → B → C) (λ (x1 : A) (x2 : B), F1 x1 x2) (λ (x1 : A) (x2 : B), F2 x1 x2) :=
|
|
|
|
|
@Abst A
|
|
|
|
|
(λ x : A, B → C)
|
|
|
|
|
(λ (x1 : A) (x2 : B), F1 x1 x2)
|
|
|
|
|
(λ (x1 : A) (x2 : B), F2 x1 x2)
|
|
|
|
|
(λ a : A, @Abst B (λ x : B, C) (λ x2 : B, F1 a x2) (λ x2 : B, F2 a x2) (λ b : B, H a b))
|
