---

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

.....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+)
BY
{ (SplitOnConclITE THEN Auto) }

1
.....truecase..... 
1. I : Cname List
2. x : nameset(I+)
3. x = fresh-cname(I) ∈ Cname
⊢ x = fresh-cname(I) ∈ extd-nameset(I+)

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  I  :  Cname  List
2.  x  :  nameset(I+)
\mvdash{}  x  =  if  eq-cname(x;fresh-cname(I))  then  fresh-cname(I)  else  x  fi 


By

---

Latex:
(SplitOnConclITE  THEN  Auto)

---

Home Index