---

Step * of Lemma case-endpoints_wf

No Annotations
∀[G:j⊢]. ∀[A:{G ⊢ _}]. ∀[a,b:{G ⊢ _:A}]. ∀[r:{G ⊢ _:𝕀}].  ([r=0 ⊢→ a; r=1 ⊢→ b] ∈ {G, ((r=0) ∨ (r=1)) ⊢ _:A})
BY
{ (Intros
   THEN Unfold `case-endpoints` 0
   THEN InstLemma `case-term_wf` [⌜G⌝;⌜(r=0)⌝;⌜(r=1)⌝;⌜A⌝;⌜a⌝;⌜b⌝]⋅
   THEN Auto
   THEN UnfoldTopAb 0
   THEN SubsumeC ⌜{G, 0(𝔽) ⊢ _:A}⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A:\{G  \mvdash{}  \_\}].  \mforall{}[a,b:\{G  \mvdash{}  \_:A\}].  \mforall{}[r:\{G  \mvdash{}  \_:\mBbbI{}\}].
    ([r=0  \mvdash{}\mrightarrow{}  a;  r=1  \mvdash{}\mrightarrow{}  b]  \mmember{}  \{G,  ((r=0)  \mvee{}  (r=1))  \mvdash{}  \_:A\})


By

---

Latex:
(Intros
  THEN  Unfold  `case-endpoints`  0
  THEN  InstLemma  `case-term\_wf`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}(r=0)\mkleeneclose{};\mkleeneopen{}(r=1)\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  UnfoldTopAb  0
  THEN  SubsumeC  \mkleeneopen{}\{G,  0(\mBbbF{})  \mvdash{}  \_:A\}\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index