---

Step * of Lemma fun-path-cons

∀[T:Type]. ∀[f:T ⟶ T]. ∀[L:T List]. ∀[x,y,z:T].
  uiff(z=f*(x) via [y / L];{(z = y ∈ T)
  ∧ ((y = (f hd(L)) ∈ T) ∧ (¬(y = hd(L) ∈ T))) ∧ hd(L)=f*(x) via L supposing 0 < ||L||
  ∧ x = y ∈ T supposing ¬0 < ||L||})
BY
{ xxx((UnivCD THENA Auto) THEN DVar `L')xxx }

1
1. T : Type
2. f : T ⟶ T
3. x : T
4. y : T
5. z : T
⊢ uiff(z=f*(x) via [y];{(z = y ∈ T)
∧ ((y = (f hd([])) ∈ T) ∧ (¬(y = hd([]) ∈ T))) ∧ hd([])=f*(x) via [] supposing 0 < ||[]||
∧ x = y ∈ T supposing ¬0 < ||[]||})

2
1. T : Type
2. f : T ⟶ T
3. u : T
4. v : T List
5. x : T
6. y : T
7. z : T
⊢ uiff(z=f*(x) via [y; [u / v]];{(z = y ∈ T)
∧ ((y = (f hd([u / v])) ∈ T) ∧ (¬(y = hd([u / v]) ∈ T))) ∧ hd([u / v])=f*(x) via [u / v] supposing 0 < ||[u / v]||
∧ x = y ∈ T supposing ¬0 < ||[u / v]||})

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  T].  \mforall{}[L:T  List].  \mforall{}[x,y,z:T].
    uiff(z=f*(x)  via  [y  /  L];\{(z  =  y)
    \mwedge{}  ((y  =  (f  hd(L)))  \mwedge{}  (\mneg{}(y  =  hd(L))))  \mwedge{}  hd(L)=f*(x)  via  L  supposing  0  <  ||L||
    \mwedge{}  x  =  y  supposing  \mneg{}0  <  ||L||\})


By

---

Latex:
xxx((UnivCD  THENA  Auto)  THEN  DVar  `L')xxx

---

Home Index