---

Step * of Lemma context-iterated-subset

No Annotations
∀[Gamma:j⊢]. ∀[phi,psi:{Gamma ⊢ _:𝔽}].
  (sub_cubical_set{j:l}(Gamma, (phi ∧ psi); Gamma, psi, phi)
  ∧ sub_cubical_set{j:l}(Gamma, psi, phi; Gamma, (phi ∧ psi)))
BY
{ (Auto
   THEN (BLemma `implies-sub_cubical_set` THENW Auto)
   THEN Intros
   THEN All
   (RepUR ``context-subset``)⋅
   THEN (Fold `member` 0 ORELSE (D 0 THENA Auto))
   THEN RepeatFor 2 (DSetVars)
   THEN ((RWO "face-and-eq-1" (-1) THEN Auto) ORELSE ((MemTypeCD THEN Auto) THEN RWO "face-and-eq-1" 0 THEN Auto))) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi,psi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].
    (sub\_cubical\_set\{j:l\}(Gamma,  (phi  \mwedge{}  psi);  Gamma,  psi,  phi)
    \mwedge{}  sub\_cubical\_set\{j:l\}(Gamma,  psi,  phi;  Gamma,  (phi  \mwedge{}  psi)))


By

---

Latex:
(Auto
  THEN  (BLemma  `implies-sub\_cubical\_set`  THENW  Auto)
  THEN  Intros
  THEN  All
  (RepUR  ``context-subset``)\mcdot{}
  THEN  (Fold  `member`  0  ORELSE  (D  0  THENA  Auto))
  THEN  RepeatFor  2  (DSetVars)
  THEN  ((RWO  "face-and-eq-1"  (-1)  THEN  Auto)
  ORELSE  ((MemTypeCD  THEN  Auto)  THEN  RWO  "face-and-eq-1"  0  THEN  Auto)
  ))

---

Home Index