---

Step * of Lemma uniform-comp-function-cumulativity

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[comp:composition-function{[i | j]:l, i:l}(Gamma; A)].
  (uniform-comp-function{[i | j]:l, i:l}(Gamma; A; comp) ⇒ uniform-comp-function{j:l, i:l}(Gamma; A; comp))
BY
{ (Auto THEN RepeatFor 6 (ParallelLast)) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[comp:composition-function\{[i  |  j]:l,  i:l\}(Gamma;  A)].
    (uniform-comp-function\{[i  |  j]:l,  i:l\}(Gamma;  A;  comp)
    {}\mRightarrow{}  uniform-comp-function\{j:l,  i:l\}(Gamma;  A;  comp))


By

---

Latex:
(Auto  THEN  RepeatFor  6  (ParallelLast))

---

Home Index