---

Step * of Lemma rename-one-extend-id

∀I:Cname List. ∀z,z1:Cname.
  ((¬(z ∈ I)) ⇒ (¬(z1 ∈ I)) ⇒ (rename-one-name(z;z1) = 1[z:=z1] ∈ name-morph([z / I];[z1 / I])))
BY
{ (Auto
   THEN BLemma `name-morphs-equal`
   THEN Auto
   THEN (FunExt THENA Auto)
   THEN RepUR ``rename-one-name extend-name-morph id-morph`` 0
   THEN (BoolCase ⌜eq-cname(x;z)⌝⋅ THENA Auto)
   THEN Fold `member` 0) }

1
1. I : Cname List
2. z : Cname
3. z1 : Cname
4. ¬(z ∈ I)
5. ¬(z1 ∈ I)
6. x : nameset([z / I])
7. x = z ∈ Cname
⊢ z1 ∈ extd-nameset([z1 / I])

2
1. I : Cname List
2. z : Cname
3. z1 : Cname
4. ¬(z ∈ I)
5. ¬(z1 ∈ I)
6. x : nameset([z / I])
7. ¬(x = z ∈ Cname)
⊢ x ∈ extd-nameset([z1 / I])

---

Latex:

---

Latex:
\mforall{}I:Cname  List.  \mforall{}z,z1:Cname.    ((\mneg{}(z  \mmember{}  I))  {}\mRightarrow{}  (\mneg{}(z1  \mmember{}  I))  {}\mRightarrow{}  (rename-one-name(z;z1)  =  1[z:=z1]))


By

---

Latex:
(Auto
  THEN  BLemma  `name-morphs-equal`
  THEN  Auto
  THEN  (FunExt  THENA  Auto)
  THEN  RepUR  ``rename-one-name  extend-name-morph  id-morph``  0
  THEN  (BoolCase  \mkleeneopen{}eq-cname(x;z)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Fold  `member`  0)

---

Home Index