---

Step * 1 2 1 of Lemma face-maps-commute


1. I : {Cname List}
2. x : ℤ
3. 2 ≤ x
4. (x ∈ I)
5. i : ℤ
6. 0 ≤ i
7. i < 2
8. y : ℤ
9. 2 ≤ y
10. (y ∈ I)
11. j : ℤ
12. 0 ≤ j
13. j < 2
14. (y:=j) ∈ name-morph(I-[x];I-[x; y])
15. a : ℤ
16. 2 ≤ a
17. (a ∈ I)
18. a = x ∈ ℤ
19. a = y ∈ ℤ
20. x = y ∈ ℤ
⊢ y = y ∈ Cname
BY
{ (D 6 THEN RevHypSubst' (-1) 0 THEN RevHypSubst' (-2) 0 THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  \{Cname  List\}
2.  x  :  \mBbbZ{}
3.  2  \mleq{}  x
4.  (x  \mmember{}  I)
5.  i  :  \mBbbZ{}
6.  0  \mleq{}  i
7.  i  <  2
8.  y  :  \mBbbZ{}
9.  2  \mleq{}  y
10.  (y  \mmember{}  I)
11.  j  :  \mBbbZ{}
12.  0  \mleq{}  j
13.  j  <  2
14.  (y:=j)  \mmember{}  name-morph(I-[x];I-[x;  y])
15.  a  :  \mBbbZ{}
16.  2  \mleq{}  a
17.  (a  \mmember{}  I)
18.  a  =  x
19.  a  =  y
20.  x  =  y
\mvdash{}  y  =  y


By

---

Latex:
(D  6  THEN  RevHypSubst'  (-1)  0  THEN  RevHypSubst'  (-2)  0  THEN  Auto)

---

Home Index