---

Step * 1 of Lemma fun-connected-tree


1. [T] : Type
2. f : T ⟶ T
3. ∀a,b:T.  (((f a) = (f b) ∈ T) ⇒ (¬((f a) = a ∈ T)) ⇒ (¬((f b) = b ∈ T)) ⇒ (a = b ∈ T))
4. x : T
5. y : T
6. z : T
7. x = (f y) ∈ T
8. ¬(x = y ∈ T)
9. y is f*(z)
10. ∀z@0:T. (y is f*(z@0) ⇒ (z@0 is f*(z) ∨ z is f*(z@0)))
11. z@0 : T
12. x is f*(z@0)
⊢ z@0 is f*(z) ∨ z is f*(z@0)
BY
{ xxx(D -1 THEN D -2)xxx }

1
1. [T] : Type
2. f : T ⟶ T
3. ∀a,b:T.  (((f a) = (f b) ∈ T) ⇒ (¬((f a) = a ∈ T)) ⇒ (¬((f b) = b ∈ T)) ⇒ (a = b ∈ T))
4. x : T
5. y : T
6. z : T
7. x = (f y) ∈ T
8. ¬(x = y ∈ T)
9. y is f*(z)
10. ∀z@0:T. (y is f*(z@0) ⇒ (z@0 is f*(z) ∨ z is f*(z@0)))
11. z@0 : T
12. x=f*(z@0) via []
⊢ z@0 is f*(z) ∨ z is f*(z@0)

2
1. [T] : Type
2. f : T ⟶ T
3. ∀a,b:T.  (((f a) = (f b) ∈ T) ⇒ (¬((f a) = a ∈ T)) ⇒ (¬((f b) = b ∈ T)) ⇒ (a = b ∈ T))
4. x : T
5. y : T
6. z : T
7. x = (f y) ∈ T
8. ¬(x = y ∈ T)
9. y is f*(z)
10. ∀z@0:T. (y is f*(z@0) ⇒ (z@0 is f*(z) ∨ z is f*(z@0)))
11. z@0 : T
12. u : T
13. v : T List
14. x=f*(z@0) via [u / v]
⊢ z@0 is f*(z) ∨ z is f*(z@0)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  f  :  T  {}\mrightarrow{}  T
3.  \mforall{}a,b:T.    (((f  a)  =  (f  b))  {}\mRightarrow{}  (\mneg{}((f  a)  =  a))  {}\mRightarrow{}  (\mneg{}((f  b)  =  b))  {}\mRightarrow{}  (a  =  b))
4.  x  :  T
5.  y  :  T
6.  z  :  T
7.  x  =  (f  y)
8.  \mneg{}(x  =  y)
9.  y  is  f*(z)
10.  \mforall{}z@0:T.  (y  is  f*(z@0)  {}\mRightarrow{}  (z@0  is  f*(z)  \mvee{}  z  is  f*(z@0)))
11.  z@0  :  T
12.  x  is  f*(z@0)
\mvdash{}  z@0  is  f*(z)  \mvee{}  z  is  f*(z@0)


By

---

Latex:
xxx(D  -1  THEN  D  -2)xxx

---

Home Index