---

Step * of Lemma rename-one-same

∀I:Cname List. ∀z:Cname.  rename-one-name(z;z) = 1 ∈ name-morph([z / I];[z / I]) supposing ¬(z ∈ I)
BY
{ (Auto
   THEN BLemma `name-morphs-equal`
   THEN Auto
   THEN (FunExt THENA Auto)
   THEN RepUR ``id-morph rename-one-name`` 0
   THEN AutoSplit
   THEN HypSubst'(-1) 0
   THEN SubsumeC ⌜nameset([z / I])⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}I:Cname  List.  \mforall{}z:Cname.    rename-one-name(z;z)  =  1  supposing  \mneg{}(z  \mmember{}  I)


By

---

Latex:
(Auto
  THEN  BLemma  `name-morphs-equal`
  THEN  Auto
  THEN  (FunExt  THENA  Auto)
  THEN  RepUR  ``id-morph  rename-one-name``  0
  THEN  AutoSplit
  THEN  HypSubst'(-1)  0
  THEN  SubsumeC  \mkleeneopen{}nameset([z  /  I])\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index