---

Step * 1 of Lemma list_eq-sq-list-deq


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]
BY
{ ((RWO "4" 0 THENA Auto) THEN (Unfold `list-deq` 0 THEN Reduce 0) THEN Trivial) }

---

Latex:

---

Latex:

1.  eq  :  Top
2.  u  :  Top
3.  v  :  Top  List
4.  \mforall{}[bs:Top  List].  (list\_eq(eq;v;bs)  \msim{}  list-deq(eq)  v  bs)
5.  u1  :  Top
6.  v1  :  Top  List
7.  list\_eq(eq;[u  /  v];v1)  \msim{}  list-deq(eq)  [u  /  v]  v1
\mvdash{}  (eq  u  u1)  \mwedge{}\msubb{}  list\_eq(eq;v;v1)  \msim{}  list-deq(eq)  [u  /  v]  [u1  /  v1]


By

---

Latex:
((RWO  "4"  0  THENA  Auto)  THEN  (Unfold  `list-deq`  0  THEN  Reduce  0)  THEN  Trivial)

---

Home Index