---

Step * of Lemma sqequal-append-cbva-weak2

∀[a:Top List]. ∀[b,F:Top].  (let x ⟵ a @ b in F[x] ~ let u ⟵ a in let v ⟵ b in let x ⟵ u @ v in F[x])
BY
{ InductionOnList }

1
∀[b,F:Top].  (let x ⟵ [] @ b in F[x] ~ let u ⟵ [] in let v ⟵ b in let x ⟵ u @ v in F[x])

2
1. u : Top
2. v : Top List
3. ∀[b,F:Top].  (let x ⟵ v @ b in F[x] ~ let u ⟵ v in let v ⟵ b in let x ⟵ u @ v in F[x])
⊢ ∀[b,F:Top].  (let x ⟵ [u / v] @ b in F[x] ~ let u ⟵ [u / v] in let v ⟵ b in let x ⟵ u @ v in F[x])

---

Latex:

---

Latex:
\mforall{}[a:Top  List].  \mforall{}[b,F:Top].
    (let  x  \mleftarrow{}{}  a  @  b
      in  F[x]  \msim{}  let  u  \mleftarrow{}{}  a
                          in  let  v  \mleftarrow{}{}  b
                                in  let  x  \mleftarrow{}{}  u  @  v
                                      in  F[x])


By

---

Latex:
InductionOnList

---

Home Index