---

Step * 1 1 of Lemma ps-sigma-elim-equality-rule

.....fun wf..... 
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. T : {X.Σ A B ⊢ _}
6. t1 : {X.A.B ⊢ _:(T)SigmaUnElim}
7. t2 : {X.A.B ⊢ _:(T)SigmaUnElim}
8. t1 = t2 ∈ {X.A.B ⊢ _:(T)SigmaUnElim}
9. Z : {X.A.B ⊢ _:(T)SigmaUnElim}
⊢ (Z)SigmaElim = (Z)SigmaElim ∈ {X.Σ A B ⊢ _:T}
BY
{ (Fold `member` 0 THEN BLemma `ps-sigma-elim-rule` THEN Auto) }

---

Latex:

---

Latex:
.....fun  wf..... 
1.  C  :  SmallCategory
2.  X  :  ps\_context\{j:l\}(C)
3.  A  :  \{X  \mvdash{}  \_\}
4.  B  :  \{X.A  \mvdash{}  \_\}
5.  T  :  \{X.\mSigma{}  A  B  \mvdash{}  \_\}
6.  t1  :  \{X.A.B  \mvdash{}  \_:(T)SigmaUnElim\}
7.  t2  :  \{X.A.B  \mvdash{}  \_:(T)SigmaUnElim\}
8.  t1  =  t2
9.  Z  :  \{X.A.B  \mvdash{}  \_:(T)SigmaUnElim\}
\mvdash{}  (Z)SigmaElim  =  (Z)SigmaElim


By

---

Latex:
(Fold  `member`  0  THEN  BLemma  `ps-sigma-elim-rule`  THEN  Auto)

---

Home Index