---

Step * of Lemma glue-term-subset

No Annotations
∀[Gamma:j⊢]. ∀[A,phi,T,t,a,xx:Top].  (Gamma, xx ⊢ glue [phi ⊢→ t] a ~ Gamma ⊢ glue [phi ⊢→ t] a)
BY
{ (Intros THEN RepUR ``glue-term context-subset`` 0 THEN Trivial ⋅) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A,phi,T,t,a,xx:Top].    (Gamma,  xx  \mvdash{}  glue  [phi  \mvdash{}\mrightarrow{}  t]  a  \msim{}  Gamma  \mvdash{}  glue  [phi  \mvdash{}\mrightarrow{}  t]  a)


By

---

Latex:
(Intros  THEN  RepUR  ``glue-term  context-subset``  0  THEN  Trivial  \mcdot{})

---

Home Index