---

Step * 1 2 of Lemma name-morph-flips-commute


1. I : Cname List
2. x : name-morph(I;[])
3. i : nameset(I)
4. j : nameset(I)
5. x1 : nameset(I)
6. (flip(flip(x;j);i) x1) = (flip(flip(x;i);j) x1) ∈ ℕ2
⊢ (flip(flip(x;j);i) x1) = (flip(flip(x;i);j) x1) ∈ extd-nameset([])
BY
{ (HypSubst' (-1)0 THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  x  :  name-morph(I;[])
3.  i  :  nameset(I)
4.  j  :  nameset(I)
5.  x1  :  nameset(I)
6.  (flip(flip(x;j);i)  x1)  =  (flip(flip(x;i);j)  x1)
\mvdash{}  (flip(flip(x;j);i)  x1)  =  (flip(flip(x;i);j)  x1)


By

---

Latex:
(HypSubst'  (-1)0  THEN  Auto)

---

Home Index