58 lines
2.4 KiB
Text
58 lines
2.4 KiB
Text
succ
|
||
((⟨nat.rec
|
||
⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ),
|
||
(λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1),
|
||
nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), a)
|
||
(λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (succ a_1)), succ ((_F.fst).fst a))
|
||
_F)
|
||
a_1
|
||
a
|
||
_F)
|
||
0
|
||
punit.star,
|
||
punit.star⟩
|
||
(λ (n : ℕ) (ih : pprod ((λ (a : ℕ), ℕ → ℕ) n) (nat.below (λ (a : ℕ), ℕ → ℕ) n)),
|
||
⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ),
|
||
(λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1),
|
||
nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), a)
|
||
(λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (succ a_1)), succ ((_F.fst).fst a))
|
||
_F)
|
||
a_1
|
||
a
|
||
_F)
|
||
(succ n)
|
||
⟨ih, punit.star⟩,
|
||
⟨ih, punit.star⟩⟩)
|
||
0,
|
||
punit.star⟩.fst).fst
|
||
2)
|
||
3
|
||
succ
|
||
((⟨nat.rec
|
||
⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ),
|
||
(λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1),
|
||
nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), a)
|
||
(λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (succ a_1)), succ ((_F.fst).fst a))
|
||
_F)
|
||
a_1
|
||
a
|
||
_F)
|
||
0
|
||
punit.star,
|
||
punit.star⟩
|
||
(λ (n : ℕ) (ih : pprod ((λ (a : ℕ), ℕ → ℕ) n) (nat.below (λ (a : ℕ), ℕ → ℕ) n)),
|
||
⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ),
|
||
(λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1),
|
||
nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), a)
|
||
(λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (succ a_1)), succ ((_F.fst).fst a))
|
||
_F)
|
||
a_1
|
||
a
|
||
_F)
|
||
(succ n)
|
||
⟨ih, punit.star⟩,
|
||
⟨ih, punit.star⟩⟩)
|
||
0,
|
||
punit.star⟩.fst).fst
|
||
a)
|
||
succ a
|