---

Step * 1 of Lemma lg-label_wf


1. T : Type
2. g : self:Top List ⋂ (T × ℕ||self|| List × (ℕ||self|| List)) List
3. x : ℕ||g||
⊢ g ∈ (T × Top) List
BY
{ (DepIsectHD 2
   THEN (Assert ||g|| ∈ ℤ BY
               (GenConcl ⌜g = L ∈ (Top List)⌝⋅ THEN Auto))
   THEN SubsumeC ⌜(T × ℕ||g|| List × (ℕ||g|| List)) List⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  g  :  self:Top  List  \mcap{}  (T  \mtimes{}  \mBbbN{}||self||  List  \mtimes{}  (\mBbbN{}||self||  List))  List
3.  x  :  \mBbbN{}||g||
\mvdash{}  g  \mmember{}  (T  \mtimes{}  Top)  List


By

---

Latex:
(DepIsectHD  2
  THEN  (Assert  ||g||  \mmember{}  \mBbbZ{}  BY
                          (GenConcl  \mkleeneopen{}g  =  L\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  SubsumeC  \mkleeneopen{}(T  \mtimes{}  \mBbbN{}||g||  List  \mtimes{}  (\mBbbN{}||g||  List))  List\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index