---

Step * 1 of Lemma name-morph-extend-id


1. I : Cname List
⊢ 1 = (1)+ ∈ (nameset(I+) ⟶ extd-nameset(I+))
BY
{ (RepUR ``id-morph name-morph-extend`` 0
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN Fold `eq-cname` 0
   THEN EqCD
   THEN Auto) }

1
.....subterm..... T:t
1:n
1. I : Cname List
2. x : nameset(I+)
⊢ x = if eq-cname(x;fresh-cname(I)) then fresh-cname(I) else x fi  ∈ extd-nameset(I+)

---

Latex:

---

Latex:

1.  I  :  Cname  List
\mvdash{}  1  =  (1)+


By

---

Latex:
(RepUR  ``id-morph  name-morph-extend``  0
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  Fold  `eq-cname`  0
  THEN  EqCD
  THEN  Auto)

---

Home Index