---

Step * 1 1 of Lemma fun-connected_weakening_eq


1. [T] : Type
2. f : T ⟶ T
3. x : T
4. y : T
5. x = y ∈ T
⊢ y=f*(x) via [x]
BY
{ ((D 0 THEN RepUR ``last`` 0) THEN Auto') }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  f  :  T  {}\mrightarrow{}  T
3.  x  :  T
4.  y  :  T
5.  x  =  y
\mvdash{}  y=f*(x)  via  [x]


By

---

Latex:
((D  0  THEN  RepUR  ``last``  0)  THEN  Auto')

---

Home Index