---

Step * of Lemma sub-presheaf-set-true

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)].  X | I,rho.True ≡ X
BY
{ (Auto
   THEN RepUR ``ext-eq-psc sub-presheaf-set`` 0
   THEN (InstLemma `presheaf-subset-true` [⌜parm{[i | j]'}⌝]⋅ THEN BHyp -1)
   THEN Auto) }

1
.....wf..... 
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. ∀[C:small-category{[i | j]':l}]. ∀[F:presheaf{[i | j]':l}(C)].  ext-equal-presheaves(C;F|True;F)
⊢ X ∈ presheaf{[i | j]':l}(C)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].    X  |  I,rho.True  \mequiv{}  X


By

---

Latex:
(Auto
  THEN  RepUR  ``ext-eq-psc  sub-presheaf-set``  0
  THEN  (InstLemma  `presheaf-subset-true`  [\mkleeneopen{}parm\{[i  |  j]'\}\mkleeneclose{}]\mcdot{}  THEN  BHyp  -1)
  THEN  Auto)

---

Home Index