---

Step * 1 of Lemma fun-path-append


1. T : Type
2. f : T ⟶ T
⊢ ∀[L2:T List]. ∀[x,y,z@0:T].  uiff(z@0=f*(x) via [] @ [y / L2];{y=f*(x) via [y / L2] ∧ z@0=f*(y) via [] @ [y]})
BY
{ (RepUR ``guard`` 0 THEN Auto) }

1
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]

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  T
\mvdash{}  \mforall{}[L2:T  List].  \mforall{}[x,y,z@0:T].
        uiff(z@0=f*(x)  via  []  @  [y  /  L2];\{y=f*(x)  via  [y  /  L2]  \mwedge{}  z@0=f*(y)  via  []  @  [y]\})


By

---

Latex:
(RepUR  ``guard``  0  THEN  Auto)

---

Home Index