---

Step * 2 1 1 1 of Lemma fun-path-append


1. T : Type
2. f : T ⟶ T
3. u : T
4. v : T List
5. ∀[L2:T List]. ∀[x,y,z:T].  uiff(z=f*(x) via v @ [y / L2];{y=f*(x) via [y / L2] ∧ z=f*(y) via v @ [y]})
6. L2 : T List
7. ∀[x,y,z:T].  uiff(z=f*(x) via v @ [y / L2];{y=f*(x) via [y / L2] ∧ z=f*(y) via v @ [y]})
8. x : T
9. ∀[y,z:T].  uiff(z=f*(x) via v @ [y / L2];{y=f*(x) via [y / L2] ∧ z=f*(y) via v @ [y]})
10. y : T
11. z : T
12. z=f*(x) via [u / (v @ [y / L2])]
⊢ {y=f*(x) via [y / L2] ∧ z=f*(y) via [u / (v @ [y])]}
BY
{ ((RWO "fun-path-cons" (-1) THENA Auto') THEN Subst' hd(v @ [y / L2]) ~ hd(v @ [y]) -1) }

1
.....equality..... 
1. T : Type
2. f : T ⟶ T
3. u : T
4. v : T List
5. ∀[L2:T List]. ∀[x,y,z:T].  uiff(z=f*(x) via v @ [y / L2];{y=f*(x) via [y / L2] ∧ z=f*(y) via v @ [y]})
6. L2 : T List
7. ∀[x,y,z:T].  uiff(z=f*(x) via v @ [y / L2];{y=f*(x) via [y / L2] ∧ z=f*(y) via v @ [y]})
8. x : T
9. ∀[y,z:T].  uiff(z=f*(x) via v @ [y / L2];{y=f*(x) via [y / L2] ∧ z=f*(y) via v @ [y]})
10. y : T
11. z : T
12. {(z = u ∈ T)
∧ ((u = (f hd(v @ [y / L2])) ∈ T) ∧ (¬(u = hd(v @ [y / L2]) ∈ T))) ∧ hd(v @ [y / L2])=f*(x) via v @ [y / L2] 
  supposing 0 < ||v @ [y / L2]||
∧ x = u ∈ T supposing ¬0 < ||v @ [y / L2]||}
⊢ hd(v @ [y / L2]) ~ hd(v @ [y])

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

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  T
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}[L2:T  List].  \mforall{}[x,y,z:T].
          uiff(z=f*(x)  via  v  @  [y  /  L2];\{y=f*(x)  via  [y  /  L2]  \mwedge{}  z=f*(y)  via  v  @  [y]\})
6.  L2  :  T  List
7.  \mforall{}[x,y,z:T].    uiff(z=f*(x)  via  v  @  [y  /  L2];\{y=f*(x)  via  [y  /  L2]  \mwedge{}  z=f*(y)  via  v  @  [y]\})
8.  x  :  T
9.  \mforall{}[y,z:T].    uiff(z=f*(x)  via  v  @  [y  /  L2];\{y=f*(x)  via  [y  /  L2]  \mwedge{}  z=f*(y)  via  v  @  [y]\})
10.  y  :  T
11.  z  :  T
12.  z=f*(x)  via  [u  /  (v  @  [y  /  L2])]
\mvdash{}  \{y=f*(x)  via  [y  /  L2]  \mwedge{}  z=f*(y)  via  [u  /  (v  @  [y])]\}


By

---

Latex:
((RWO  "fun-path-cons"  (-1)  THENA  Auto')  THEN  Subst'  hd(v  @  [y  /  L2])  \msim{}  hd(v  @  [y])  -1)

---

Home Index