---

Step * of Lemma fun-path-append

No Annotations
∀[T:Type]. ∀[f:T ⟶ T]. ∀[L1,L2:T List]. ∀[x,y,z:T].
  uiff(z=f*(x) via L1 @ [y / L2];{y=f*(x) via [y / L2] ∧ z=f*(y) via L1 @ [y]})
BY
{ TACTIC:InductionOnList }

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

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]})
⊢ ∀[L2:T List]. ∀[x,y,z:T].  uiff(z=f*(x) via [u / v] @ [y / L2];{y=f*(x) via [y / L2] ∧ z=f*(y) via [u / v] @ [y]})

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  T].  \mforall{}[L1,L2:T  List].  \mforall{}[x,y,z:T].
    uiff(z=f*(x)  via  L1  @  [y  /  L2];\{y=f*(x)  via  [y  /  L2]  \mwedge{}  z=f*(y)  via  L1  @  [y]\})


By

---

Latex:
TACTIC:InductionOnList

---

Home Index