---

Step * 1 2 1 2 1 of Lemma face-maps-comp-property

.....subterm..... T:t
1:n
1. L : (Cname × ℕ2) List
2. L1 : (Cname × ℕ2) List
3. I : Cname List
⊢ nameset(map(λp.(fst(p));L1) @ I) ∈ Type
BY
{ TACTIC:Auto }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  L  :  (Cname  \mtimes{}  \mBbbN{}2)  List
2.  L1  :  (Cname  \mtimes{}  \mBbbN{}2)  List
3.  I  :  Cname  List
\mvdash{}  nameset(map(\mlambda{}p.(fst(p));L1)  @  I)  \mmember{}  Type


By

---

Latex:
TACTIC:Auto

---

Home Index