Step
*
of Lemma
uniform-extend-contractible
No Annotations
∀Gamma:j⊢. ∀A:{Gamma ⊢ _}. ∀ext:Gamma +⊢ Extension(A). {Gamma ⊢ _:Contractible(A)}
BY
{ (Intros THEN UseWitness ⌜extend-to-contraction(Gamma;A;ext)⌝⋅ THEN Auto) }
Latex:
Latex:
No Annotations
\mforall{}Gamma:j\mvdash{}. \mforall{}A:\{Gamma \mvdash{} \_\}. \mforall{}ext:Gamma +\mvdash{} Extension(A). \{Gamma \mvdash{} \_:Contractible(A)\}
By
Latex:
(Intros THEN UseWitness \mkleeneopen{}extend-to-contraction(Gamma;A;ext)\mkleeneclose{}\mcdot{} THEN Auto)
Home
Index