---

Step * of Lemma context-adjoin-subset4

No Annotations
∀[H:j⊢]. ∀[phi:{H ⊢ _:𝔽}].
  ∀T:{H ⊢j _}. ∀[psi:{H.T ⊢ _:𝔽}]. ((psi = (phi)p ∈ {H.T ⊢ _:𝔽}) ⇒ sub_cubical_set{j:l}(H, phi.T; H.T, psi))
BY
{ ((InstLemma `context-adjoin-subset3` [⌜parm{j}⌝;⌜parm{j}⌝;⌜parm{j}⌝]⋅ THEN RepeatFor 3 (ParallelLast))
   THEN Intros
   THEN RWO  "-1" 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H:j\mvdash{}].  \mforall{}[phi:\{H  \mvdash{}  \_:\mBbbF{}\}].
    \mforall{}T:\{H  \mvdash{}j  \_\}.  \mforall{}[psi:\{H.T  \mvdash{}  \_:\mBbbF{}\}].  ((psi  =  (phi)p)  {}\mRightarrow{}  sub\_cubical\_set\{j:l\}(H,  phi.T;  H.T,  psi))


By

---

Latex:
((InstLemma  `context-adjoin-subset3`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{j\}\mkleeneclose{}]\mcdot{}
    THEN  RepeatFor  3  (ParallelLast)
    )
  THEN  Intros
  THEN  RWO    "-1"  0
  THEN  Auto)

---

Home Index