---

Step * of Lemma term-context-subset-subtype

No Annotations
∀[Gamma:j⊢]. ∀[phi1,phi2:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma ⊢ _}].
  {Gamma, phi1 ⊢ _:A} ⊆r {Gamma, phi2 ⊢ _:A} supposing Gamma ⊢ (phi2 ⇒ phi1)
BY
{ (Intros THEN BLemma `subset-cubical-term` THEN Auto THEN BLemma `face-term-implies-subset` THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi1,phi2:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].
    \{Gamma,  phi1  \mvdash{}  \_:A\}  \msubseteq{}r  \{Gamma,  phi2  \mvdash{}  \_:A\}  supposing  Gamma  \mvdash{}  (phi2  {}\mRightarrow{}  phi1)


By

---

Latex:
(Intros
  THEN  BLemma  `subset-cubical-term`
  THEN  Auto
  THEN  BLemma  `face-term-implies-subset`
  THEN  Auto)

---

Home Index