---

Step * 1 of Lemma list_decomp_reverse


1. [T] : Type
2. u : T
3. v : T List
4. ∃x:T. ∃L':T List. (v = (L' @ [x]) ∈ (T List)) supposing 0 < ||v||
⊢ ∃x:T. ∃L':T List. ([u / v] = (L' @ [x]) ∈ (T List))
BY
{ DVar `v' }

1
1. [T] : Type
2. u : T
3. ∃x:T. ∃L':T List. ([] = (L' @ [x]) ∈ (T List)) supposing 0 < ||[]||
⊢ ∃x:T. ∃L':T List. ([u] = (L' @ [x]) ∈ (T List))

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

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  u  :  T
3.  v  :  T  List
4.  \mexists{}x:T.  \mexists{}L':T  List.  (v  =  (L'  @  [x]))  supposing  0  <  ||v||
\mvdash{}  \mexists{}x:T.  \mexists{}L':T  List.  ([u  /  v]  =  (L'  @  [x]))


By

---

Latex:
DVar  `v'

---

Home Index