---

Step * of Lemma context-iterated-subset0

No Annotations
∀[X:j⊢]. ∀[xx,yy:{X ⊢ _:𝔽}].  sub_cubical_set{j:l}(X, xx, yy; X)
BY
{ (Auto THEN Using [`Y',⌜X, (yy ∧ xx)⌝] (BLemma `sub_cubical_set_transitivity`)⋅ 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)


By

---

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

---

Home Index