---

Step * of Lemma csm+_wf+

No Annotations
∀[H,K:j⊢]. ∀[A:{H ⊢ _}]. ∀[tau:K ij⟶ H]. ∀[B:{H.A ⊢ _}].  (tau++ ∈ K.(A)tau.(B)tau+ ij⟶ H.A.B)
BY
{ (InstLemma `csm+_wf` []
   THEN RepeatFor 4 (ParallelLast')
   THEN Intro
   THEN InstLemmaIJ `csm+_wf` [⌜H.A⌝;⌜K.(A)tau⌝;⌜B⌝;⌜tau+⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H,K:j\mvdash{}].  \mforall{}[A:\{H  \mvdash{}  \_\}].  \mforall{}[tau:K  ij{}\mrightarrow{}  H].  \mforall{}[B:\{H.A  \mvdash{}  \_\}].    (tau++  \mmember{}  K.(A)tau.(B)tau+  ij{}\mrightarrow{}  H.A.B)


By

---

Latex:
(InstLemma  `csm+\_wf`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  Intro
  THEN  InstLemmaIJ  `csm+\_wf`  [\mkleeneopen{}H.A\mkleeneclose{};\mkleeneopen{}K.(A)tau\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}tau+\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index