---

Step * of Lemma presheaf-pair-eta

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[w:{X ⊢ _:Σ A B}].
  (presheaf-pair(w.1;w.2) = w ∈ {X ⊢ _:Σ A B})
BY
{ (Intros
   THEN Symmetry
   THEN BLemma `presheaf-term-equal`
   THEN ((RepeatFor 2 ((Ext THENA Auto))
          THEN RepUR ``presheaf-sigma presheaf-pair`` 0
          THEN RepUR ``presheaf-fst presheaf-snd`` 0
          THEN DVar `w'
          THEN RepUR ``presheaf-sigma`` 5
          THEN GenConclAtAddr [2]
          THEN DVar `v'
          THEN Reduce 0
          THEN Auto)
   ORELSE Auto
   )) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[B:\{X.A  \mvdash{}  \_\}].  \mforall{}[w:\{X  \mvdash{}  \_:\mSigma{}  A  B\}].
    (presheaf-pair(w.1;w.2)  =  w)


By

---

Latex:
(Intros
  THEN  Symmetry
  THEN  BLemma  `presheaf-term-equal`
  THEN  ((RepeatFor  2  ((Ext  THENA  Auto))
                THEN  RepUR  ``presheaf-sigma  presheaf-pair``  0
                THEN  RepUR  ``presheaf-fst  presheaf-snd``  0
                THEN  DVar  `w'
                THEN  RepUR  ``presheaf-sigma``  5
                THEN  GenConclAtAddr  [2]
                THEN  DVar  `v'
                THEN  Reduce  0
                THEN  Auto)
  ORELSE  Auto
  ))

---

Home Index