---

Step * 1 1 of Lemma fix-connected


1. T : Type
2. eq : EqDecider(T)
3. f : T ⟶ T
4. retraction(T;f)
5. x : T
6. y : T
7. z : T
8. x = (f y) ∈ T
9. ¬(x = y ∈ T)
10. y is f*(z)
11. f**(y) = f**(z) ∈ T
⊢ f**(x) = f**(z) ∈ T
BY
{ (HypSubst (-4) 0 THENA Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. f : T ⟶ T
4. retraction(T;f)
5. x : T
6. y : T
7. z : T
8. x = (f y) ∈ T
9. ¬(x = y ∈ T)
10. y is f*(z)
11. f**(y) = f**(z) ∈ T
⊢ f**(f y) = f**(z) ∈ T

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  f  :  T  {}\mrightarrow{}  T
4.  retraction(T;f)
5.  x  :  T
6.  y  :  T
7.  z  :  T
8.  x  =  (f  y)
9.  \mneg{}(x  =  y)
10.  y  is  f*(z)
11.  f**(y)  =  f**(z)
\mvdash{}  f**(x)  =  f**(z)


By

---

Latex:
(HypSubst  (-4)  0  THENA  Auto)

---

Home Index