---

Step * of Lemma lift-reduce-face-map

No Annotations
∀[I:Cname List]. ∀[x:nameset(I)]. ∀[c,i:ℕ2].
  ((iota(fresh-cname(I)) o ((x:=i) o (fresh-cname(I):=c))) = (x:=i) ∈ name-morph(I;I-[x]))
BY
{ (Auto THEN (GenConclTerm ⌜fresh-cname(I)⌝⋅ THENA Auto) THEN Thin (-1) THEN D -1) }

1
1. I : Cname List
2. x : nameset(I)
3. c : ℕ2
4. i : ℕ2
5. v : Cname
6. ¬(v ∈ I)
⊢ (iota(v) o ((x:=i) o (v:=c))) = (x:=i) ∈ name-morph(I;I-[x])

---

Latex:

---

Latex:
No  Annotations
\mforall{}[I:Cname  List].  \mforall{}[x:nameset(I)].  \mforall{}[c,i:\mBbbN{}2].
    ((iota(fresh-cname(I))  o  ((x:=i)  o  (fresh-cname(I):=c)))  =  (x:=i))


By

---

Latex:
(Auto  THEN  (GenConclTerm  \mkleeneopen{}fresh-cname(I)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Thin  (-1)  THEN  D  -1)

---

Home Index