---

Step * of Lemma csm-id-adjoin_wf-interval-1

No Annotations
∀[Gamma:j⊢]. ([1(𝕀)] ∈ Gamma j⟶ Gamma.𝕀)
BY
{ (Intro THEN InstLemma `csm-id-adjoin_wf` [⌜parm{j}⌝;⌜parm{j}⌝;⌜Gamma⌝;⌜𝕀⌝;⌜1(𝕀)⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  ([1(\mBbbI{})]  \mmember{}  Gamma  j{}\mrightarrow{}  Gamma.\mBbbI{})


By

---

Latex:
(Intro  THEN  InstLemma  `csm-id-adjoin\_wf`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}\mBbbI{}\mkleeneclose{};\mkleeneopen{}1(\mBbbI{})\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index