---

Step * of Lemma iota-face-map

∀[I:Cname List]. ∀[x,y:Cname]. ∀[i:ℕ2].
  ((x:=i) o iota(y)) = (iota(y) o (x:=i)) ∈ name-morph(I;[y / I-[x]]) supposing ¬(x = y ∈ Cname)
BY
{ (Auto THEN BLemma `name-morphs-equal` THEN Try ((Using [`J',⌜I-[x]⌝] MemCD⋅ THEN Auto))) }

1
.....wf..... 
1. I : Cname List
2. x : Cname
3. y : Cname
4. i : ℕ2
5. ¬(x = y ∈ Cname)
⊢ (iota(y) o (x:=i)) ∈ nameset(I) ⟶ extd-nameset([y / I-[x]])

2
1. I : Cname List
2. x : Cname
3. y : Cname
4. i : ℕ2
5. ¬(x = y ∈ Cname)
⊢ ((x:=i) o iota(y)) = (iota(y) o (x:=i)) ∈ (nameset(I) ⟶ extd-nameset([y / I-[x]]))

---

Latex:

---

Latex:
\mforall{}[I:Cname  List].  \mforall{}[x,y:Cname].  \mforall{}[i:\mBbbN{}2].    ((x:=i)  o  iota(y))  =  (iota(y)  o  (x:=i))  supposing  \mneg{}(x  =  y)


By

---

Latex:
(Auto  THEN  BLemma  `name-morphs-equal`  THEN  Try  ((Using  [`J',\mkleeneopen{}I-[x]\mkleeneclose{}]  MemCD\mcdot{}  THEN  Auto)))

---

Home Index