---

Step * of Lemma filling-function_wf

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}].  (filling-function{j:l, i:l}(Gamma;A) ∈ 𝕌{[i' | j'']})
BY
{ (Intros
   THEN Unfold `filling-function` 0
   THEN (MemCD THENL [Complete (Auto); (InstLemma `cube_set_map_wf` [⌜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{}  \_\}].    (filling-function\{j:l,  i:l\}(Gamma;A)  \mmember{}  \mBbbU{}\{[i'  |  j'']\})


By

---

Latex:
(Intros
  THEN  Unfold  `filling-function`  0
  THEN  (MemCD  THENL  [Complete  (Auto);  (InstLemma  `cube\_set\_map\_wf`  [\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