---

Step * of Lemma name-morph-flips-commute

∀I:Cname List. ∀x:name-morph(I;[]). ∀i,j:nameset(I).  (flip(flip(x;j);i) = flip(flip(x;i);j) ∈ name-morph(I;[]))
BY
{ (Auto THEN BLemma `name-morph-ext` THEN Auto) }

1
1. I : Cname List
2. x : name-morph(I;[])
3. i : nameset(I)
4. j : nameset(I)
5. x1 : nameset(I)
⊢ (flip(flip(x;j);i) x1) = (flip(flip(x;i);j) x1) ∈ extd-nameset([])

---

Latex:

---

Latex:
\mforall{}I:Cname  List.  \mforall{}x:name-morph(I;[]).  \mforall{}i,j:nameset(I).    (flip(flip(x;j);i)  =  flip(flip(x;i);j))


By

---

Latex:
(Auto  THEN  BLemma  `name-morph-ext`  THEN  Auto)

---

Home Index