---

Step * 1 1 of Lemma fun-path-append


1. T : Type
2. f : T ⟶ T
3. L2 : T List
4. x : T
5. y : T
6. z@0 : T
7. z@0=f*(x) via [y / L2]
⊢ z@0=f*(y) via [y]
BY
{ (RepUR ``fun-path last`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  T
3.  L2  :  T  List
4.  x  :  T
5.  y  :  T
6.  z@0  :  T
7.  z@0=f*(x)  via  [y  /  L2]
\mvdash{}  z@0=f*(y)  via  [y]


By

---

Latex:
(RepUR  ``fun-path  last``  0  THEN  Auto)

---

Home Index