---

Step * 2 1 of Lemma ulist-ext


1. T : Type
⊢ [] ∈ ulist(T)
BY
{ TACTIC:(RepUR ``ulist urec nil it`` 0 THEN (MemTypeCDUnion ⌜1⌝⋅ THEN Auto) THEN BUnionLeft THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
\mvdash{}  []  \mmember{}  ulist(T)


By

---

Latex:
TACTIC:(RepUR  ``ulist  urec  nil  it``  0
                THEN  (MemTypeCDUnion  \mkleeneopen{}1\mkleeneclose{}\mcdot{}  THEN  Auto)
                THEN  BUnionLeft
                THEN  Auto)

---

Home Index