---

Step * of Lemma rename-one-iota

∀I:Cname List. ∀z,z1:Cname.
  (iota(z) o rename-one-name(z;z1)) = iota(z1) ∈ name-morph(I;[z1 / I]) supposing (¬(z1 ∈ I)) ∧ (¬(z ∈ I))
BY
{ (Auto THEN (Symmetry THEN BLemma `name-morphs-equal` THEN Auto)) }

1
.....wf..... 
1. I : Cname List
2. z : Cname
3. z1 : Cname
4. ¬(z1 ∈ I)
5. ¬(z ∈ I)
⊢ (iota(z) o rename-one-name(z;z1)) ∈ nameset(I) ⟶ extd-nameset([z1 / I])

2
1. I : Cname List
2. z : Cname
3. z1 : Cname
4. ¬(z1 ∈ I)
5. ¬(z ∈ I)
⊢ iota(z1) = (iota(z) o rename-one-name(z;z1)) ∈ (nameset(I) ⟶ extd-nameset([z1 / I]))

---

Latex:

---

Latex:
\mforall{}I:Cname  List.  \mforall{}z,z1:Cname.
    (iota(z)  o  rename-one-name(z;z1))  =  iota(z1)  supposing  (\mneg{}(z1  \mmember{}  I))  \mwedge{}  (\mneg{}(z  \mmember{}  I))


By

---

Latex:
(Auto  THEN  (Symmetry  THEN  BLemma  `name-morphs-equal`  THEN  Auto))

---

Home Index