---

Step * of Lemma contractibilty-of-singleton

No Annotations
∀X:j⊢. ∀A:{X ⊢ _}. ∀a:{X ⊢ _:A}.  {X ⊢ _:Contractible(Singleton(a))}
BY
{ (Auto THEN UseWitness ⌜singleton-contr(X;A;a)⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}X:j\mvdash{}.  \mforall{}A:\{X  \mvdash{}  \_\}.  \mforall{}a:\{X  \mvdash{}  \_:A\}.    \{X  \mvdash{}  \_:Contractible(Singleton(a))\}


By

---

Latex:
(Auto  THEN  UseWitness  \mkleeneopen{}singleton-contr(X;A;a)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index