---

Step * of Lemma name-morph-flip-face-map

∀I:Cname List. ∀y:nameset(I). ∀a:ℕ2. ∀c1:name-morph(I;[]). ∀v:nameset(I).
  ((¬(v = y ∈ Cname)) ⇒ (flip(((y:=a) o c1);v) = ((y:=a) o flip(c1;v)) ∈ name-morph(I;[])))
BY
{ (InstLemma  `name-morph-flip-face-map1` [] THEN RepeatFor 4 (ParallelLast')) }

---

Latex:

---

Latex:
\mforall{}I:Cname  List.  \mforall{}y:nameset(I).  \mforall{}a:\mBbbN{}2.  \mforall{}c1:name-morph(I;[]).  \mforall{}v:nameset(I).
    ((\mneg{}(v  =  y))  {}\mRightarrow{}  (flip(((y:=a)  o  c1);v)  =  ((y:=a)  o  flip(c1;v))))


By

---

Latex:
(InstLemma    `name-morph-flip-face-map1`  []  THEN  RepeatFor  4  (ParallelLast'))

---

Home Index