---

Step * 1 of Lemma lg-remove_wf


1. T : Type
2. g : self:Top List ∩ (T × ℕ||self|| List × (ℕ||self|| List)) List
3. g ∈ Top List
4. g ∈ (T × ℕ||g|| List × (ℕ||g|| List)) List
5. ||g|| ∈ ℕ
6. x : ℕ
⊢ lg-remove(g;x) ∈ Top List
BY
{ ProveWfLemma }

---

Latex:

---

Latex:

1.  T  :  Type
2.  g  :  self:Top  List  \mcap{}  (T  \mtimes{}  \mBbbN{}||self||  List  \mtimes{}  (\mBbbN{}||self||  List))  List
3.  g  \mmember{}  Top  List
4.  g  \mmember{}  (T  \mtimes{}  \mBbbN{}||g||  List  \mtimes{}  (\mBbbN{}||g||  List))  List
5.  ||g||  \mmember{}  \mBbbN{}
6.  x  :  \mBbbN{}
\mvdash{}  lg-remove(g;x)  \mmember{}  Top  List


By

---

Latex:
ProveWfLemma

---

Home Index