---

Step * of Lemma composition-structure-cumulativity

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}].  (Gamma +⊢ Compositon(A) ⊆r Gamma ⊢ Compositon(A))
BY
{ (Auto THEN (D 0 THENA Auto) THEN RepeatFor 2 (ParallelLast) THEN (RepeatFor 5 (ParallelLast) ORELSE Auto)) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].    (Gamma  +\mvdash{}  Compositon(A)  \msubseteq{}r  Gamma  \mvdash{}  Compositon(A))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  (RepeatFor  5  (ParallelLast)  ORELSE  Auto))

---

Home Index