---

Step * of Lemma context-iterated-subset1

No Annotations
∀[X:j⊢]. ∀[xx,yy:{X ⊢ _:𝔽}].  sub_cubical_set{j:l}(X, xx, yy; X, yy)
BY
{ (Auto
   THEN (Using [`Y',⌜X, (yy ∧ xx)⌝] (BLemma `sub_cubical_set_transitivity`)⋅ THEN Auto)
   THEN BLemma `face-term-implies-subset`
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[xx,yy:\{X  \mvdash{}  \_:\mBbbF{}\}].    sub\_cubical\_set\{j:l\}(X,  xx,  yy;  X,  yy)


By

---

Latex:
(Auto
  THEN  (Using  [`Y',\mkleeneopen{}X,  (yy  \mwedge{}  xx)\mkleeneclose{}]  (BLemma  `sub\_cubical\_set\_transitivity`)\mcdot{}  THEN  Auto)
  THEN  BLemma  `face-term-implies-subset`
  THEN  Auto)

---

Home Index