28 lines
1,003 B
Text
28 lines
1,003 B
Text
Assumed: f
|
||
Assumed: N
|
||
Assumed: n1
|
||
Assumed: n2
|
||
Set option: lean::pp::implicit
|
||
f::explicit N n1 n2
|
||
f::explicit ((N [33m→[0m N) [33m→[0m N [33m→[0m N) ([33mλ[0m x : N [33m→[0m N, x) ([33mλ[0m y : N [33m→[0m N, y)
|
||
Assumed: EqNice
|
||
EqNice::explicit N n1 n2
|
||
N
|
||
[33mΠ[0m (A : [36mType[0m u) (B : A [33m→[0m [36mType[0m u) (f g : [33mΠ[0m x : A, B x) (a b : A) (H1 : f = g) (H2 : a = b), (f a) = (g b)
|
||
f::explicit N n1 n2
|
||
Assumed: a
|
||
Assumed: b
|
||
Assumed: c
|
||
Assumed: g
|
||
Assumed: H1
|
||
Proved: Pr
|
||
[34mAxiom[0m H1 : a = b ∧ b = c
|
||
[34mTheorem[0m Pr : (g a) = (g c) [33m:=[0m
|
||
[33mlet[0m κ::1 [33m:=[0m Trans::explicit
|
||
N
|
||
a
|
||
b
|
||
c
|
||
(Conjunct1::explicit (a = b) (b = c) H1)
|
||
(Conjunct2::explicit (a = b) (b = c) H1)
|
||
[33min[0m Congr::explicit N ([33mλ[0m x : N, N) g g a c (Refl::explicit (N [33m→[0m N) g) κ::1
|