---

Step * 1 2 1 1 of Lemma list_decomp_reverse


1. T : Type
2. u : T
3. u1 : T
4. v : T List
5. x : T
6. L' : T List
7. [u1 / v] = (L' @ [x]) ∈ (T List)
⊢ [u; [u1 / v]] = ([u / L'] @ [x]) ∈ (T List)
BY
{ ((Reduce 0 THEN EqCD) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T
3.  u1  :  T
4.  v  :  T  List
5.  x  :  T
6.  L'  :  T  List
7.  [u1  /  v]  =  (L'  @  [x])
\mvdash{}  [u;  [u1  /  v]]  =  ([u  /  L']  @  [x])


By

---

Latex:
((Reduce  0  THEN  EqCD)  THEN  Auto)

---

Home Index