---

Step * 1 2 1 of Lemma list_decomp_reverse


1. [T] : Type
2. u : T
3. u1 : T
4. v : T List
5. ∃x:T. ∃L':T List. ([u1 / v] = (L' @ [x]) ∈ (T List))
⊢ ∃x:T. ∃L':T List. ([u; [u1 / v]] = (L' @ [x]) ∈ (T List))
BY
{ ((ExRepD THEN InstConcl [x;[u / L']]) THEN Auto) }

1
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)

---

Latex:

---

Latex:

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


By

---

Latex:
((ExRepD  THEN  InstConcl  [x;[u  /  L']])  THEN  Auto)

---

Home Index