---

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:


\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

InductionOnList

---

Home Index