---

Step * of Lemma psc-m2_wf

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}].  (q2 ∈ {X.A.B ⊢ _:((A)p)p})
BY
{ (Intros
   THEN Unfold `psc-m2` 0
   THEN (InstLemma `psc-snd_wf` [⌜C⌝;⌜X⌝;⌜A⌝]⋅ THENA Auto)
   THEN (GenConclTerm  ⌜q⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN Thin (-2)
   THEN Unhide
   THEN MoveToConcl (-1)
   THEN GenConcl ⌜(A)p = Z ∈ {X.A ⊢ _}⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[B:\{X.A  \mvdash{}  \_\}].
    (q2  \mmember{}  \{X.A.B  \mvdash{}  \_:((A)p)p\})


By

---

Latex:
(Intros
  THEN  Unfold  `psc-m2`  0
  THEN  (InstLemma  `psc-snd\_wf`  [\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (GenConclTerm    \mkleeneopen{}q\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  Thin  (-2)
  THEN  Unhide
  THEN  MoveToConcl  (-1)
  THEN  GenConcl  \mkleeneopen{}(A)p  =  Z\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index