---

Step * of Lemma composition-function-cumulativity

No Annotations
∀Gamma:j⊢. ∀Z:{Gamma ⊢ _}.  (composition-function{[i | j]:l, i:l}(Gamma; Z) ⊆r composition-function{j:l,i:l}(Gamma;Z))
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN ParallelLast
   THEN RepeatFor 2 ((FunExt THENA Auto))
   THEN RepeatFor 2 ((MemCD THENL [Id; Auto]))
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}Gamma:j\mvdash{}.  \mforall{}Z:\{Gamma  \mvdash{}  \_\}.
    (composition-function\{[i  |  j]:l,  i:l\}(Gamma;  Z)  \msubseteq{}r  composition-function\{j:l,i:l\}(Gamma;Z))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  ParallelLast
  THEN  RepeatFor  2  ((FunExt  THENA  Auto))
  THEN  RepeatFor  2  ((MemCD  THENL  [Id;  Auto]))
  THEN  Auto)

---

Home Index