Step * of Lemma cc-snd_wf

No Annotations
[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}].  (q ∈ {Gamma.A ⊢ _:(A)p})
BY
PresheafMLTTInstance Obid: psc-snd_wf⋅ }


Latex:


Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].    (q  \mmember{}  \{Gamma.A  \mvdash{}  \_:(A)p\})


By


Latex:
PresheafMLTTInstance  Obid:  psc-snd\_wf\mcdot{}




Home Index