---

Step * 1 of Lemma ps-sigma-unelim-elim


1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. I : cat-ob(C)
6. a1 : X(I)
7. a2 : A(a1)
8. x1 : B(<a1, a2>)
⊢ <<a1, a2>, x1> = <<a1, a2>, x1> ∈ (alpha:alpha:X(I) × A(alpha) × B(alpha))
BY
{ (Fold `member` 0 THEN MemCD THEN Auto THEN RepUR ``psc-adjoin`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  X  :  ps\_context\{j:l\}(C)
3.  A  :  \{X  \mvdash{}  \_\}
4.  B  :  \{X.A  \mvdash{}  \_\}
5.  I  :  cat-ob(C)
6.  a1  :  X(I)
7.  a2  :  A(a1)
8.  x1  :  B(<a1,  a2>)
\mvdash{}  <<a1,  a2>,  x1>  =  <<a1,  a2>,  x1>


By

---

Latex:
(Fold  `member`  0  THEN  MemCD  THEN  Auto  THEN  RepUR  ``psc-adjoin``  0  THEN  Auto)

---

Home Index