---

Step * of Lemma list_eq-sq-list-deq

∀[eq:Top]. ∀[as,bs:Top List].  (list_eq(eq;as;bs) ~ list-deq(eq) as bs)
BY
{ (RepeatFor 2 (InductionOnList) THEN Unfold `list_eq` 0 THEN Reduce 0 THEN Auto) }

1
1. eq : Top
2. u : Top
3. v : Top List
4. ∀[bs:Top List]. (list_eq(eq;v;bs) ~ list-deq(eq) v bs)
5. u1 : Top
6. v1 : Top List
7. list_eq(eq;[u / v];v1) ~ list-deq(eq) [u / v] v1
⊢ (eq u u1) ∧b list_eq(eq;v;v1) ~ list-deq(eq) [u / v] [u1 / v1]

---

Latex:

---

Latex:
\mforall{}[eq:Top].  \mforall{}[as,bs:Top  List].    (list\_eq(eq;as;bs)  \msim{}  list-deq(eq)  as  bs)


By

---

Latex:
(RepeatFor  2  (InductionOnList)  THEN  Unfold  `list\_eq`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index