---

Step * of Lemma thin-context-subset

No Annotations
∀[Gamma:j⊢]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[t:{Gamma ⊢ _}].  Gamma, phi ⊢ t
BY
{ (InstLemma `context-subset-subtype-simple` [] THEN RepeatFor 2 (ParallelLast') THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[t:\{Gamma  \mvdash{}  \_\}].    Gamma,  phi  \mvdash{}  t


By

---

Latex:
(InstLemma  `context-subset-subtype-simple`  []  THEN  RepeatFor  2  (ParallelLast')  THEN  Auto)

---

Home Index