---

Step * of Lemma name-morph-nil

∀[I:Cname List]. name-morph(I;[]) ≡ nameset(I) ⟶ ℕ2
BY
{ (Auto THEN RepeatFor 2 ((D 0 THENA Auto))) }

1
.....subterm..... T:t
1:n
1. I : Cname List
2. x : name-morph(I;[])
⊢ x ∈ nameset(I) ⟶ ℕ2

2
.....subterm..... T:t
1:n
1. I : Cname List
2. x : nameset(I) ⟶ ℕ2
⊢ x ∈ name-morph(I;[])

---

Latex:

---

Latex:
\mforall{}[I:Cname  List].  name-morph(I;[])  \mequiv{}  nameset(I)  {}\mrightarrow{}  \mBbbN{}2


By

---

Latex:
(Auto  THEN  RepeatFor  2  ((D  0  THENA  Auto)))

---

Home Index