Step
*
of Lemma
empty-context-lemma
No Annotations
∀[Gamma:j⊢]. ∀[A,x:Top]. (x ∈ {Gamma ⊢ _:A}) supposing ∀I:fset(ℕ). (¬Gamma(I))
BY
{ (Intros THEN Unfold `member` 0 THEN InstLemma `empty-context-eq-lemma` [⌜Gamma⌝;⌜A⌝;⌜x⌝;⌜x⌝]⋅ THEN Auto) }
Latex:
Latex:
No Annotations
\mforall{}[Gamma:j\mvdash{}]. \mforall{}[A,x:Top]. (x \mmember{} \{Gamma \mvdash{} \_:A\}) supposing \mforall{}I:fset(\mBbbN{}). (\mneg{}Gamma(I))
By
Latex:
(Intros
THEN Unfold `member` 0
THEN InstLemma `empty-context-eq-lemma` [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
THEN Auto)
Home
Index