---

Step * 1 of Lemma fun-path-append1


1. T : Type
2. f : T ⟶ T
⊢ ∀[x,y,z:T].  (z=f*(x) via [x]) supposing ((¬(y = x ∈ T)) and (y = (f x) ∈ T) and z=f*(y) via [])
BY
{ (Auto THEN D -3 THEN All Reduce THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  T
\mvdash{}  \mforall{}[x,y,z:T].    (z=f*(x)  via  [x])  supposing  ((\mneg{}(y  =  x))  and  (y  =  (f  x))  and  z=f*(y)  via  [])


By

---

Latex:
(Auto  THEN  D  -3  THEN  All  Reduce  THEN  Auto)

---

Home Index