---

Step * 2 1 1 1 1 2 1 1 1 of Lemma CCC-bool


1. B : ℕ
2. h : f:(ℕB ⟶ 𝔹) ⟶ ℕB
⊢ (∀f,g:ℕB ⟶ 𝔹.  (((h f) = (h g) ∈ ℤ) ⇒ f (h f) = g (h g))) ⇒ False
BY
{ (NatInd 1 THEN Auto) }

1
1. B : ℤ
2. h : f:(ℕ0 ⟶ 𝔹) ⟶ ℕ0
3. ∀f,g:ℕ0 ⟶ 𝔹.  (((h f) = (h g) ∈ ℤ) ⇒ f (h f) = g (h g))
⊢ False

2
1. B : ℤ
2. 0 < B
3. ∀h:f:(ℕB - 1 ⟶ 𝔹) ⟶ ℕB - 1. ((∀f,g:ℕB - 1 ⟶ 𝔹.  (((h f) = (h g) ∈ ℤ) ⇒ f (h f) = g (h g))) ⇒ False)
4. h : f:(ℕB ⟶ 𝔹) ⟶ ℕB
5. ∀f,g:ℕB ⟶ 𝔹.  (((h f) = (h g) ∈ ℤ) ⇒ f (h f) = g (h g))
⊢ False

---

Latex:

---

Latex:

1.  B  :  \mBbbN{}
2.  h  :  f:(\mBbbN{}B  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbN{}B
\mvdash{}  (\mforall{}f,g:\mBbbN{}B  {}\mrightarrow{}  \mBbbB{}.    (((h  f)  =  (h  g))  {}\mRightarrow{}  f  (h  f)  =  g  (h  g)))  {}\mRightarrow{}  False


By

---

Latex:
(NatInd  1  THEN  Auto)

---

Home Index