---

Step * 1 2 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)) supposing 0 < ||[u1 / v]||
⊢ ∃x:T. ∃L':T List. ([u; [u1 / v]] = (L' @ [x]) ∈ (T List))
BY
{ (D -1 THENA Auto) }

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

---

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]))  supposing  0  <  ||[u1  /  v]||
\mvdash{}  \mexists{}x:T.  \mexists{}L':T  List.  ([u;  [u1  /  v]]  =  (L'  @  [x]))


By

---

Latex:
(D  -1  THENA  Auto)

---

Home Index