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