---

Step * of Lemma composition-function_wf

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}].  (composition-function{j:l,i:l}(Gamma;A) ∈ 𝕌{[i' | j'']})
BY
{ (Intros
   THEN Unfold `composition-function` 0
   THEN (MemCD THENL [Complete (Auto); (InstLemma `cube_set_map_wf` [⌜parm{j}⌝;⌜H.𝕀⌝;⌜Gamma⌝]⋅ THENA Auto)])
   THEN (MemCD THENL [(DoSubsume THEN Auto); Id])
   THEN (MemCD THENL [Complete (Auto); Id])
   THEN (MemCD THENL [(Auto THEN SubsumeC ⌜H, phi.𝕀 j⟶ Gamma⌝⋅ THEN Auto); Id])
   THEN MemCD
   THEN MemCD
   THEN Try (Complete (Auto))
   THEN InferEqualTypeUp
   THEN Auto
   THEN SubsumeC ⌜H, phi.𝕀 j⟶ Gamma⌝⋅
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  Unfold  `composition-function`  0
  THEN  (MemCD
              THENL  [Complete  (Auto);  (InstLemma  `cube\_set\_map\_wf`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}H.\mBbbI{}\mkleeneclose{};\mkleeneopen{}Gamma\mkleeneclose{}]\mcdot{}  THENA  Auto)]
  )
  THEN  (MemCD  THENL  [(DoSubsume  THEN  Auto);  Id])
  THEN  (MemCD  THENL  [Complete  (Auto);  Id])
  THEN  (MemCD  THENL  [(Auto  THEN  SubsumeC  \mkleeneopen{}H,  phi.\mBbbI{}  j{}\mrightarrow{}  Gamma\mkleeneclose{}\mcdot{}  THEN  Auto);  Id])
  THEN  MemCD
  THEN  MemCD
  THEN  Try  (Complete  (Auto))
  THEN  InferEqualTypeUp
  THEN  Auto
  THEN  SubsumeC  \mkleeneopen{}H,  phi.\mBbbI{}  j{}\mrightarrow{}  Gamma\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index