---

Step * of Lemma face-map-idempotent

∀A,B:Cname List. ∀x:nameset(A). ∀g:name-morph(A-[x];B). ∀i:ℕ2.
  (((x:=i) o ((x:=i) o g)) = ((x:=i) o g) ∈ name-morph(A;B))
BY
{ (Auto
   THEN BLemma `face-map-comp-id`
   THEN Auto
   THEN RepUR ``name-comp face-map`` 0
   THEN (BoolCase ⌜(x =z x)⌝⋅ THENA Auto)
   THEN Try ((D 4 THEN Fold `member` 0 THEN Auto))
   THEN OnVar  `i' IntSegCases
   THEN RepUR ``uext isname`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}A,B:Cname  List.  \mforall{}x:nameset(A).  \mforall{}g:name-morph(A-[x];B).  \mforall{}i:\mBbbN{}2.
    (((x:=i)  o  ((x:=i)  o  g))  =  ((x:=i)  o  g))


By

---

Latex:
(Auto
  THEN  BLemma  `face-map-comp-id`
  THEN  Auto
  THEN  RepUR  ``name-comp  face-map``  0
  THEN  (BoolCase  \mkleeneopen{}(x  =\msubz{}  x)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  ((D  4  THEN  Fold  `member`  0  THEN  Auto))
  THEN  OnVar    `i'  IntSegCases
  THEN  RepUR  ``uext  isname``  0
  THEN  Auto)

---

Home Index