---

Step * of Lemma contractible-uniform-extend

No Annotations
∀Gamma:j⊢. ∀A:{Gamma ⊢ _}. ∀cA:Gamma ⊢ Compositon(A). ∀ctr:{Gamma ⊢ _:Contractible(A)}.  Gamma ⊢ Extension(A)
BY
{ (Intros THEN UseWitness ⌜contraction-to-extend(Gamma;A;cA;ctr)⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}Gamma:j\mvdash{}.  \mforall{}A:\{Gamma  \mvdash{}  \_\}.  \mforall{}cA:Gamma  \mvdash{}  Compositon(A).  \mforall{}ctr:\{Gamma  \mvdash{}  \_:Contractible(A)\}.
    Gamma  \mvdash{}  Extension(A)


By

---

Latex:
(Intros  THEN  UseWitness  \mkleeneopen{}contraction-to-extend(Gamma;A;cA;ctr)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index